Theorems · Theorem · group theory
dvd_zero
∀ {α : Type u_1} [inst : SemigroupWithZero α] (a : α), a ∣ 0- Cited by
- 63 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses propext
- 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.mul_zeroproof · cited by 2,091
- Dvd.introproof · cited by 26
- SemigroupWithZerostatement and proof · cited by 6
Cited by63
Results whose statement or proof uses this declaration.
- UniqueFactorizationMonoid.dvd_of_mem_normalizedFactorsproof · cited by 20
- Nat.dvd_of_mem_primeFactorsListproof · cited by 8
- EuclideanDomain.gcd_dvdproof · cited by 8
- UniqueFactorizationMonoid.radical_dvd_selfproof · cited by 7
- addOrderOf_dvd_natCardproof · cited by 6
- Polynomial.IsPrimitive.ne_zeroproof · cited by 4
- PadicInt.appr_specproof · cited by 4
- Multiset.dvd_sumproof · cited by 4
- Nat.dvd_of_primeFactorsList_subpermproof · cited by 4
- Valuation.Integers.dvd_of_leproof · cited by 4
- dvdNotUnit_of_dvd_of_not_dvdproof · cited by 4
- AddMonoid.exponent_dvd_iff_forall_nsmul_eq_zeroproof · cited by 4