Commit 2025-12-12 12:04 17bd7deb

View on Github →

feat(Algebra): define Dedekind-finite monoids (every left inverse is also a right inverse) (#32610)

  • Prove equivalent characterizations of Dedekind-finite monoids.
  • Show commutative monoids, finite monoids, and Artinian semirings are Dedekind-finite, and finite monoids/rings are Dedekind-finite.

Estimated changes

added theorem mul_eq_one_comm
modified theorem MulOpposite.op_pow
modified theorem MulOpposite.op_zpow
modified theorem MulOpposite.unop_pow
modified theorem MulOpposite.unop_zpow
modified theorem IsUnit.mul_iff
modified theorem IsUnit.of_mul_eq_one
modified theorem IsUnit.of_mul_eq_one_right
modified def Units.mkOfMulEqOne
modified theorem Units.val_mkOfMulEqOne
modified theorem isUnit_iff_exists_inv'
modified theorem isUnit_iff_exists_inv
modified theorem isUnit_of_mul_isUnit_left
modified theorem isUnit_of_mul_isUnit_right