Mathlib Map

Theorems · Theorem · group theory

DivisibleHull.coe_injective

∀ {M : Type u_1} [inst : AddCommMonoid M] [IsAddTorsionFree M], Function.Injective DivisibleHull.coe
Defined in
Mathlib.GroupTheory.DivisibleHull
Cited by
2 results in Mathlib
Foundations
Depth 36 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
AddCommMonoidIsAddTorsionFree
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

DivisibleHull.coe_inj · cited by 0DivisibleHull.coe_injhahnEmbedding_isOrderedAddMonoid · cited by 0hahnEmbedding_isOrderedAd…AddCommMonoid · cited by 12281AddCommMonoidIsAddTorsionFree · cited by 155IsAddTorsionFreeDivisibleHull · cited by 30DivisibleHullDivisibleHull.coe · cited by 5DivisibleHull.coeDivisibleHull.mk_left_injective · cited by 1DivisibleHull.mk_left_inj…DivisibleHull.coe_injectiveCITED BYCITES

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by2

Results whose statement or proof uses this declaration.