normHom — Mathlib

English

The real norm function on a normed ring extends to a MonoidWithZeroHom from α to ℝ, with the standard properties: norm(0)=0, norm(1)=1, norm(x y)=norm(x) norm(y).

Русский

Функция нормы на нормированном кольце является моноидно-нулевым гомоморфизм: norm(0)=0, norm(1)=1, norm(xy)=norm(x)norm(y).

LaTeX

$$$\\text{norm}(0)=0, \\quad \\text{norm}(1)=1, \\quad \\text{norm}(xy)=\\text{norm}(x)\\text{norm}(y)$$$

Lean4

/-- `norm` as a `MonoidWithZeroHom`. -/
@[simps]
def normHom : α →*₀ ℝ where
  toFun := (‖·‖)
  map_zero' := norm_zero
  map_one' := norm_one
  map_mul' := norm_mul

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