Theorem pow_apply_eq_iterate

Modification history

2026-10-13 20:38

Mathlib/Algebra/Group/IsApply.lean

refactor(Algebra): make the arguments of `Is*Apply` implicit (#42704) …

Modified pow_apply_eq_iterate View on Github →

2026-06-23 15:06

Mathlib/Data/FunLike/IsApply.lean

feat: `Monoid` and `Group` instances for `OrderHom` and `OrderIso` (#40515) …

Added pow_apply_eq_iterate View on Github →