Commit 2026-10-28 12:53 caa0dcb1

View on Github →

feat(Algebra/Group/IsApply): new typeclass IsNPowApplyEqIterate (#45218) Create a new typeclass IsNPowApplyEqIterate, so that FunLike.compMonoidWithZero does not force consumers to use the default value npow field npowRec.

Estimated changes

Modified Mathlib/Algebra/Group/IsApply.lean

modified theorem FunLike.coe_pow_eq_iterate

deleted theorem pow_apply_eq_iterate

Modified Mathlib/Algebra/GroupWithZero/FunLike.lean

Modified Mathlib/Algebra/Ring/FunLike.lean

Modified Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean