Theorems · Definition · group theory
DivisibleHull
(M : Type u_1) → [AddCommMonoid M] → Type u_1
The divisible hull of an AddCommMonoid (as a ℕ-module) is the localized module by
ℕ+ (implemented using nonZeroDivisors ℕ), thus a ℕ-divisible group, or a ℚ≥0-module.
- Defined in
- Mathlib.GroupTheory.DivisibleHull
- Cited by
- 30 results in Mathlib
- Foundations
- Depth 26 from the axioms · uses propext, Quot.sound
- Assumes
- AddCommMonoid
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.
- AddCommMonoidstatement and proof · cited by 12,281
- nonZeroDivisorsproof · cited by 895
- LocalizedModuleproof · cited by 154
Cited by37
Results whose statement or proof uses this declaration.
- DivisibleHull.mkstatement · cited by 19
- DivisibleHull.coestatement · cited by 5
- DivisibleHull.archimedeanClassOrderIsostatement · cited by 3
- DivisibleHull.coeOrderAddMonoidHomstatement and proof · cited by 3
- DivisibleHull.mk_add_mk_leftstatement and proof · cited by 3
- DivisibleHull.coe_injectivestatement · cited by 2
- DivisibleHull.liftOnstatement and proof · cited by 2
- DivisibleHull.mk_zerostatement · cited by 2
- DivisibleHull.coeAddMonoidHomstatement · cited by 1
- DivisibleHull.coeOrderAddMonoidHom_applystatement · cited by 1
- DivisibleHull.liftOn₂statement and proof · cited by 1
- DivisibleHull.mk_add_mkstatement · cited by 1