Theorem npowRec'_succ

Modification history

2025-03-29 10:26

Mathlib/Algebra/Group/Defs.lean

feat: generalize Mathlib.Algebra.Group+Ring+Field (#23143) …

Modified npowRec'_succ View on Github →

2024-11-14 13:58

Mathlib/Algebra/Group/Defs.lean

chore(Algebra/Group/Defs): use `Nat.binaryRec` (#17892)

Modified npowRec'_succ View 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'_succ View on Github →