Theorems · Theorem · group theory
eq_zero_or_one_of_sq_eq_self
∀ {M₀ : Type u_1} [inst : MonoidWithZero M₀] [IsRightCancelMulZero M₀] {x : M₀}, x ^ 2 = x → x = 0 ∨ x = 1- Defined in
- Mathlib.Algebra.GroupWithZero.Defs
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 13 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- one_mulproof · cited by 2,841
- MonoidWithZerostatement and proof · cited by 456
- sqproof · cited by 280
- IsRightCancelMulZerostatement and proof · cited by 33
- mul_left_injective₀proof · cited by 22
Cited by4
Results whose statement or proof uses this declaration.
- IsIdempotentElem.spectrum_subsetproof · cited by 2
- IsPowMul.map_one_le_oneproof · cited by 1
- not_isCyclic_iff_exponent_eq_primeproof · cited by 0
- not_isAddCyclic_iff_exponent_eq_primeproof · cited by 0