Commit 2024-11-14 13:58 95ee83bc

View on Github →

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

Estimated changes

Modified Mathlib/Algebra/Group/Defs.lean

modified def npowBinRec

modified theorem npowRec'_mul_comm

modified theorem npowRec'_succ

deleted def nsmulBinRec

deleted theorem nsmulRec_eq_nsmulBinRec