Commit 2026-08-20 19:44 c9474400

View on Github →

refactor(Algebra/Group): split overlong file Defs.lean (#42952) Split this > 1500 line file into 5 roughly equal pieces:

  • semigroups
  • monoids
  • DivInvMonoid
  • groups
  • unbundled Is(Add/Mul)Commutative tag & associated scoped instances

Estimated changes

deleted def DivInvMonoid.div'
deleted theorem IsLeftRegular.all
deleted theorem IsRegular.all
deleted theorem IsRightRegular.all
deleted theorem MulOneClass.ext
deleted theorem MulOneClass.isUnital
deleted def SubNegMonoid.sub'
deleted theorem div_eq_mul_inv
deleted theorem eq_inv_of_mul_eq_one_left
deleted theorem exists_zpow_surjective
deleted theorem inv_eq_of_mul_eq_one_left
deleted theorem inv_eq_one_div
deleted theorem inv_inv
deleted theorem inv_one
deleted theorem isMulCommutative_iff
deleted theorem left_inv_eq_right_inv
deleted theorem mul_assoc
deleted theorem mul_comm'
deleted theorem mul_comm
deleted theorem mul_div_assoc
deleted theorem mul_eq_one_comm
deleted theorem mul_inv_rev
deleted theorem mul_left_cancel
deleted theorem mul_left_cancel_iff
deleted theorem mul_left_inj
deleted theorem mul_left_injective
deleted theorem mul_ne_mul_left
deleted theorem mul_ne_mul_right
deleted theorem mul_one
deleted theorem mul_pow_mul
deleted theorem mul_right_cancel
deleted theorem mul_right_cancel_iff
deleted theorem mul_right_inj
deleted theorem mul_right_injective
deleted theorem negSucc_zsmul
deleted theorem npowBinRec.go_spec
deleted def npowBinRec
deleted theorem npowBinRec_succ
deleted theorem npowBinRec_zero
deleted def npowRec'
deleted theorem npowRec'_mul_comm
deleted theorem npowRec'_succ
deleted theorem npowRec'_two_mul
deleted theorem npowRec_add
deleted theorem npowRec_eq
deleted theorem npowRec_eq_npowBinRec
deleted theorem npowRec_succ
deleted theorem npow_eq_pow
deleted def nsmulRec'
deleted theorem one_div
deleted theorem one_mul
deleted theorem one_pow
deleted theorem pow_add
deleted theorem pow_mul'
deleted theorem pow_mul
deleted theorem pow_mul_comm'
deleted theorem pow_mul_comm
deleted theorem pow_one
deleted theorem pow_right_comm
deleted theorem pow_succ'
deleted theorem pow_succ
deleted theorem pow_three'
deleted theorem pow_three
deleted theorem pow_two
deleted theorem pow_zero
deleted def zpowRec
deleted theorem zpow_eq_pow
deleted theorem zpow_natCast
deleted theorem zpow_negSucc
deleted theorem zpow_neg_coe_of_pos
deleted theorem zpow_neg_one
deleted theorem zpow_ofNat
deleted theorem zpow_one
deleted theorem zpow_two
deleted theorem zpow_zero
deleted def zsmulRec
added theorem div_eq_mul_inv
added theorem exists_zpow_surjective
added theorem inv_eq_one_div
added theorem inv_inv
added theorem inv_one
added theorem mul_div_assoc
added theorem mul_inv_rev
added theorem negSucc_zsmul
added theorem one_div
added def zpowRec
added theorem zpow_eq_pow
added theorem zpow_natCast
added theorem zpow_negSucc
added theorem zpow_neg_coe_of_pos
added theorem zpow_neg_one
added theorem zpow_ofNat
added theorem zpow_one
added theorem zpow_two
added theorem zpow_zero
added def zsmulRec
added theorem MulOneClass.ext
added theorem MulOneClass.isUnital
added theorem left_inv_eq_right_inv
added theorem mul_eq_one_comm
added theorem mul_one
added theorem mul_pow_mul
added theorem npowBinRec.go_spec
added def npowBinRec
added theorem npowBinRec_succ
added theorem npowBinRec_zero
added def npowRec'
added theorem npowRec'_mul_comm
added theorem npowRec'_succ
added theorem npowRec'_two_mul
added theorem npowRec_add
added theorem npowRec_eq
added theorem npowRec_eq_npowBinRec
added theorem npowRec_succ
added theorem npow_eq_pow
added def nsmulRec'
added theorem one_mul
added theorem one_pow
added theorem pow_add
added theorem pow_mul'
added theorem pow_mul
added theorem pow_mul_comm'
added theorem pow_mul_comm
added theorem pow_one
added theorem pow_right_comm
added theorem pow_succ'
added theorem pow_succ
added theorem pow_three'
added theorem pow_three
added theorem pow_two
added theorem pow_zero
added theorem IsLeftRegular.all
added theorem IsRegular.all
added theorem IsRightRegular.all
added theorem isMulCommutative_iff
added theorem mul_assoc
added theorem mul_comm'
added theorem mul_comm
added theorem mul_left_cancel
added theorem mul_left_cancel_iff
added theorem mul_left_inj
added theorem mul_left_injective
added theorem mul_ne_mul_left
added theorem mul_ne_mul_right
added theorem mul_right_cancel
added theorem mul_right_cancel_iff
added theorem mul_right_inj
added theorem mul_right_injective