instFunLike — Mathlib

English

An additive valuation is coerced to the underlying function R → Γ₀, i.e., each AddValuation acts as a map from R to Γ₀.

Русский

Аддитивная оценка приводится к функции: каждая AddValuation действует как отображение из R в Γ₀.

LaTeX

$$FunLike( AddValuation R Γ₀, R, Γ₀ )$$

Lean4

/-- A valuation is coerced to the underlying function `R → Γ₀`. -/
instance (R) (Γ₀) [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] : FunLike (AddValuation R Γ₀) R Γ₀
    where
  coe v := v.toMonoidWithZeroHom.toFun
  coe_injective' f g := by cases f; cases g; simp +contextual

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