Theorem npowRec_eq_npowBinRec

Modification history

2024-10-15 22:29
Mathlib/Algebra/Group/Defs.lean
feat: use @[csimp] to use exponentiation by repeated squaring at runtime (#8885) …
Added npowRec_eq_npowBinRecView on Github →