toMulRingNorm — Mathlib

English

The norm on a NormedField naturally forms a MulRingNorm on the field.

Русский

Норма на нормированном поле естественным образом образует MulRingNorm на поле.

LaTeX

$$$(\text{NormedField.toMulRingNorm } R)\; \text{is a } MulRingNorm R$$$

Lean4

/-- The norm on a `NormedField`, as a `MulRingNorm`. -/
def toMulRingNorm (R : Type*) [NormedField R] : MulRingNorm R
    where
  toFun := norm
  map_zero' := norm_zero
  map_one' := norm_one
  add_le' := norm_add_le
  map_mul' := norm_mul
  neg' := norm_neg
  eq_zero_of_map_eq_zero' x hx := by rw [← norm_eq_zero]; exact hx

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