Mathlib Map

Theorems · Theorem · commutative algebra

Valuation.restrict_le_iff_le_embedding

∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀)
  {x : R} {g : (MonoidWithZeroHom.ofClass v).ValueGroup₀},
  v.restrict x ≤ g ↔ v x ≤ MonoidWithZeroHom.ValueGroup₀.embedding g
Defined in
Mathlib.RingTheory.Valuation.Basic
Cited by
2 results in Mathlib
Foundations
Depth 79 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
RingLinearOrderedCommGroupWithZero
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Valuation.restrict_le_iff · cited by 6Valuation.restrict_le_iffValuation.restrict_le_one_iff · cited by 6Valuation.restrict_le_one…DFunLike.coe · cited by 62936DFunLike.coeRing · cited by 7463RingSubgroup · cited by 3593SubgroupUnits · cited by 2804UnitsValuation · cited by 823ValuationMonoidWithZeroHom · cited by 704MonoidWithZeroHomLinearOrderedCommGroupWithZero · cited by 528LinearOrderedCommGroupWit…MonoidWithZeroHom.ofClass · cited by 204MonoidWithZeroHom.ofClassMonoidWithZeroHom.valueGroup · cited by 170MonoidWithZeroHom.valueGr…MonoidWithZeroHom.ValueGroup₀ · cited by 166MonoidWithZeroHom.ValueGr…Valuation.restrict · cited by 112Valuation.restrictStrictMono.le_iff_le · cited by 104StrictMono.le_iff_leMonoidWithZeroHom.ValueGroup₀.embedding · cited by 47ValueGroup₀.embeddingMonoidWithZeroHom.ValueGroup₀.embedding_strictMono · cited by 12ValueGroup₀.embedding_str…Valuation.embedding_restrict · cited by 9Valuation.embedding_restr…Valuation.restrict_le_iff_le_…CITED BYCITES

Cites15

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.