extends_norm — Mathlib

English

If an algebra norm f satisfies f(1)=1, then for all a in R, f(a⋅1) equals the norm of a in R, i.e., f(a⋅1) = ||a||.

Русский

Если алгебраическая норма f удовлетворяет f(1)=1, то для всех a ∈ R имеет место f(a⋅1) = ||a||.

LaTeX

$$(f(1)=1) → ∀ a:\\ R, f(a\\cdot 1) = \\|a\\|$$

Lean4

/-- An `R`-algebra norm such that `f 1 = 1` extends the norm on `R`. -/
theorem extends_norm (hf1 : f 1 = 1) (a : R) : f (algebraMap R S a) = ‖a‖ := by rw [Algebra.algebraMap_eq_smul_one];
  exact extends_norm' hf1 _

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