Theorems · Theorem · commutative algebra
Valuation.Integers.hom_inj
∀ {R : Type u} {Γ₀ : Type v} [inst : CommRing R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] {v : Valuation R Γ₀}
{O : Type w} [inst_2 : CommRing O] [inst_3 : Algebra O R], v.Integers O → Function.Injective ⇑(algebraMap O R)- Defined in
- Mathlib.RingTheory.Valuation.Integers
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 16 from the axioms · uses no axioms
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.coestatement · cited by 62,936
- CommRingstatement and proof · cited by 17,173
- Algebrastatement and proof · cited by 11,388
- RingHomstatement · cited by 10,189
- Algebra.algebraMapstatement · cited by 4,706
- Valuationstatement and proof · cited by 823
- LinearOrderedCommGroupWithZerostatement and proof · cited by 528
- Valuation.Integersstatement and proof · cited by 58
Cited by14
Results whose statement or proof uses this declaration.
- Valuation.Integers.coe_span_singleton_eq_setOfPred_le_v_algebraMapproof · cited by 5
- Valuation.Integers.dvd_of_leproof · cited by 4
- Valuation.Integers.isUnit_of_oneproof · cited by 2
- Valuation.Integers.maximalIdeal_eq_setOfPred_le_v_algebraMapstatement and proof · cited by 2
- Valuation.Integers.maximalIdeal_pow_eq_setOfPred_le_v_algebraMap_powstatement and proof · cited by 2
- Valuation.Integers.nontrivial_iffproof · cited by 2
- Valuation.Integers.valuation_pos_iff_ne_zeroproof · cited by 2
- Valuation.Integers.bijective_algebraMap_of_subsingleton_units_mrangeproof · cited by 1
- Valuation.Integers.isFractionRingproof · cited by 1
- Valuation.Integers.isIntegral_iff_v_le_oneproof · cited by 1
- Valuation.Integers.isPrincipalIdealRing_iff_not_denselyOrderedproof · cited by 1
- ValuationRing.of_integersstatement and proof · cited by 1