coe_mk — Mathlib

English

The coercion constructed by Valuation.mk is identically the underlying function f: R →*₀ Γ₀ (up to the given homomorphism data).

Русский

Указательное отображение, полученное через Valuation.mk, совпадает с исходной функцией f: R →*₀ Γ₀ (с учётом данных гомоморфизма).

LaTeX

$$$\\text{coe\_mk }(f,h) : \\!\\! \\mathrm{Valuation.mk} f h = f$ (as functions).$$

Lean4

@[simp]
theorem coe_mk (f : R →*₀ Γ₀) (h) : ⇑(Valuation.mk f h) = f :=
  rfl

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