instFunLike — Mathlib

English

There is a canonical instance equipping Valuation R Γ₀ as a ValuationClass, providing the required maps for multiplication, one, zero, and the max-based addition bound.

Русский

Существует канонический инстанс, делающий Valuation R Γ₀ классом оценки, с необходимыми отображениями умножения, единицы, нуля и ограничения через max.

LaTeX

$$$\\text{Valuation.instValuationClass } : \\mathrm{ValuationClass} (\\mathrm{Valuation } R \\Gamma_0) R \\Gamma_0.$$$

Lean4

instance : FunLike (Valuation R Γ₀) R Γ₀ where
  coe f := f.toFun
  coe_injective' f g
    h := by
    obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := f
    congr

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