Structures · Algebra
IsDedekindFiniteMonoid
A monoid is Dedekind-finite if every left inverse is also a right inverse. It is more common to talk about Dedekind-finite rings, but https://arxiv.org/abs/2102.01598 does define Dedekind-finite monoids in §2.2.
- Defined in
- Mathlib.Algebra.Group.Defs
- Shape
- One type argument · adds mul_eq_one_symm
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances3
- Matrix
- Subtype
- MulOpposite
How is a type an instance?
Loading the hierarchy index…
Assumed by17
- IsUnit.of_mul_eq_one
- isUnit_iff_exists_inv
- Units.mkOfMulEqOne
- isUnit_of_mul_isUnit_left
- IsUnit.mul_iff
- isUnit_of_mul_isUnit_right
- isUnit_iff_exists_inv'
- IsDedekindFiniteMonoid.mul_eq_one_symm
- mul_eq_one_comm
- IsUnit.of_mul_eq_one_right
- IsDedekindFiniteMonoid.of_injective
- Units.val_mkOfMulEqOne
- invertibleOfRightInverse
- SubmonoidClass.instIsDedekindFiniteMonoidSubtypeMem
- invertibleOfLeftInverse
- MulOpposite.instIsDedekindFiniteMonoid
- Units.mkOfMulEqOne.congr_simp
Ancestors0
No ancestors.