Commit 2026-10-30 14:28 ae156997

View on Github →

feat: use IsApply for AddConstMap (#45351) Also add an abbrev that provides a monoid instance for a FunLike type satisfying (f * g) x = f (g x) and 1 x = x.

Estimated changes

Modified Mathlib/Algebra/AddConstMap/Basic.lean

modified theorem AddConstMap.coe_mul

modified theorem AddConstMap.coe_one

modified theorem AddConstMap.coe_pow

deleted theorem AddConstMap.pow_apply

Modified Mathlib/Algebra/Group/FunLike.lean