toMonoidWithZeroHom_one — Mathlib

English

The unit valuation acts as the identity on the associated monoid-with-zero homomorphism: the unit valuation maps 1 to 1.

Русский

Единичная валюация действует как тождественное отображение на сопутствующем однородном моноидном отображении: 1 перейдёт в 1.

LaTeX

$$$ (1 : \\mathrm{Valuation}(R,\\Gamma_0)).\\mathrm{toMonoidWithZeroHom} = 1 $$$

Lean4

@[simp]
theorem toMonoidWithZeroHom_one : (1 : Valuation R Γ₀).toMonoidWithZeroHom = 1 :=
  rfl

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