Repository navigation

feat: use `IsApply` for `AddConstMap` - #45351

Open

EtienneC30 wants to merge 5 commits into

leanprover-community:masterfrom

EtienneC30:apply-addconstmap

Open

feat: use `IsApply` for `AddConstMap`#45351
EtienneC30 wants to merge 5 commits into
leanprover-community:masterfrom
EtienneC30:apply-addconstmap

Commits on Oct 27, 2026
- feat: use `IsApply` for `AddConstMap`
  EtienneC30
  committed
  83947b4
Commits on Oct 28, 2026
- Merge branch 'master' of https://github.com/leanprover-community/mathlib4 into apply-addconstmap
  EtienneC30
  committed
  5217153
- review
  EtienneC30
  committed
  7bee932
- Merge branch 'master' of https://github.com/leanprover-community/mathlib4 into apply-addconstmap
  EtienneC30
  committed
  33bb6b5
- fix
  EtienneC30
  committed
  46d2f47