Theorem npowRec'_succ

Modification history

2026-08-20 19:44
Mathlib/Algebra/Group/Defs.lean
refactor(Algebra/Group): split overlong file Defs.lean (#42952) …
Modified npowRec'_succView on Github →
2025-03-29 10:26
Mathlib/Algebra/Group/Defs.lean
feat: generalize Mathlib.Algebra.Group+Ring+Field (#23143) …
Modified npowRec'_succView on Github →
2024-11-14 13:58
Mathlib/Algebra/Group/Defs.lean
chore(Algebra/Group/Defs): use `Nat.binaryRec` (#17892)
Modified npowRec'_succView on Github →
2024-10-15 22:29
Mathlib/Algebra/Group/Defs.lean
feat: use @[csimp] to use exponentiation by repeated squaring at runtime (#8885) …
Added npowRec'_succView on Github →