Theorems · Theorem · group theory
eq_zero_of_zero_dvd
∀ {α : Type u_1} [inst : SemigroupWithZero α] {a : α}, 0 ∣ a → a = 0- Cited by
- 13 results in Mathlib
- Foundations
- Depth 7 from the axioms · uses no axioms
- Assumes
- SemigroupWithZero
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- MulZeroClass.zero_mulproof · cited by 1,625
- SemigroupWithZerostatement and proof · cited by 6
- Dvd.elimproof · cited by 4
Cited by13
Results whose statement or proof uses this declaration.
- zero_dvd_iffproof · cited by 37
- CharP.charP_to_charZeroproof · cited by 11
- ZMod.unitsMap_surjectiveproof · cited by 7
- AddSubgroup.relIndex_eq_zero_of_le_leftproof · cited by 3
- Subgroup.relIndex_eq_zero_of_le_leftproof · cited by 3
- Multiset.gcd_eq_zero_iffproof · cited by 2
- Pell.y_dvd_iffproof · cited by 2
- Nat.totient_div_of_dvdproof · cited by 1
- Submonoid.LocalizationMap.uniqueFactorizationMonoidproof · cited by 1
- AdjoinRoot.of.injective_of_degree_ne_zeroproof · cited by 1
- IsCyclotomicExtension.le_of_dvdproof · cited by 1
- Ordinal.dvd_antisymmproof · cited by 0