Theorems · Inductive type · group theory
IsDedekindFiniteMonoid
(M : Type u_2) → [MulOne M] → Prop
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
- Cited by
- 23 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- MulOne
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- MulOnestatement · cited by 65
Cited by30
Results whose statement or proof uses this declaration.
- IsUnit.of_mul_eq_onestatement and proof · cited by 43
- isUnit_iff_exists_invstatement and proof · cited by 21
- Units.mkOfMulEqOnestatement and proof · cited by 15
- isUnit_of_mul_isUnit_leftstatement and proof · cited by 12
- isUnit_of_mul_isUnit_rightstatement and proof · cited by 8
- IsUnit.mul_iffstatement and proof · cited by 8
- isUnit_iff_exists_inv'statement and proof · cited by 8
- IsUnit.of_mul_eq_one_rightstatement and proof · cited by 5
- IsDedekindFiniteMonoid.mul_eq_one_symmstatement and proof · cited by 5
- mul_eq_one_commstatement and proof · cited by 5
- IsDedekindFiniteMonoid.of_injectivestatement and proof · cited by 3
- isDedekindFiniteMonoid_iffstatement and proof · cited by 2