ofValuation — Mathlib

English

Given a valuation v: S → Γ between rings S and Γ, there is a canonical Compatible instance, showing that v is compatible

Русский

Пусть дано оценивание v: S → Γ между кольцами S и Γ; существует канонический экземпляр Compatible, доказывающий совместимость

LaTeX

$$Valuation.Compatible.ofValuation(v) holds$$

Lean4

theorem _root_.Valuation.Compatible.ofValuation {S Γ : Type*} [CommRing S] [LinearOrderedCommGroupWithZero Γ]
    (v : Valuation S Γ) :
    letI := ValuativeRel.ofValuation v
    Valuation.Compatible v :=
  letI := ValuativeRel.ofValuation v
  ⟨fun _ _ ↦ Iff.rfl⟩

Похожие утверждения