toMonoidWithZeroHom_coe_eq_coe — Mathlib

English

Let v be a valuation on a ring R with value group Γ₀. The associated monoid-with-zero homomorphism is exactly v when viewed as a function R → Γ₀.

Русский

Пусть v — валюация кольца R со значительной группой Γ₀. Связанное отображение моноида с нулём совпадает с самой функцией v, если рассматривать как функцию R → Γ₀.

LaTeX

$$$ (v.toMonoidWithZeroHom : R \to Γ_0) = v $$$

Lean4

@[simp]
theorem toMonoidWithZeroHom_coe_eq_coe (v : Valuation R Γ₀) : (v.toMonoidWithZeroHom : R → Γ₀) = v :=
  rfl

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