Theorems · Inductive type · group theory
IsDedekindFiniteAddMonoid
(M : Type u_2) → [AddZero M] → Prop
An additive monoid is Dedekind-finite if every left inverse is also a right inverse. Also called von Neumann-finite or directly finite.
- Defined in
- Mathlib.Algebra.Group.Defs
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- AddZero
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.
- AddZerostatement · cited by 87
Cited by21
Results whose statement or proof uses this declaration.
- isAddUnit_iff_exists_negstatement and proof · cited by 4
- IsDedekindFiniteAddMonoid.add_eq_zero_symmstatement and proof · cited by 4
- IsAddUnit.of_add_eq_zerostatement and proof · cited by 3
- IsAddUnit.add_iffstatement and proof · cited by 2
- AddUnits.mkOfAddEqZerostatement and proof · cited by 2
- isDedekindFiniteAddMonoid_iffstatement and proof · cited by 1
- isAddUnit_iff_exists_neg'statement and proof · cited by 1
- isAddUnit_of_add_isAddUnit_leftstatement and proof · cited by 1
- isAddUnit_of_add_isAddUnit_rightstatement and proof · cited by 1
- IsAddUnit.of_add_eq_zero_rightstatement and proof · cited by 1
- add_eq_zero_commstatement and proof · cited by 1
- IsDedekindFiniteAddMonoid.casesOnstatement and proof · cited by 1