Theorems · Theorem · group theory
DivisibleHull.mk_zero
∀ {M : Type u_1} [inst : AddCommMonoid M] (s : ℕ+), DivisibleHull.mk 0 s = 0- Defined in
- Mathlib.GroupTheory.DivisibleHull
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 31 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- AddCommMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- AddCommMonoidstatement and proof · cited by 12,281
- nonZeroDivisorsstatement · cited by 895
- PNatstatement and proof · cited by 392
- DivisibleHullstatement · cited by 30
- DivisibleHull.mkstatement · cited by 19
- OreLocalization.zero_oreDivproof · cited by 8
- PNat.equivNonZeroDivisorsNatproof · cited by 6
Cited by2
Results whose statement or proof uses this declaration.
- DivisibleHull.neg_mkproof · cited by 0
- DivisibleHull.nsmul_mkproof · cited by 0