instUnitizationNormedRing — Mathlib

English

The unitization WithLp 1 (Unitization 𝕜 A) carries a normed ring structure.

Русский

У единичизации WithLp 1 (Unitization 𝕜 A) есть структура нормированной кольца.

LaTeX

$$$\text{NormedRing}(WithLp 1 (Unitization 𝕜 A))$$$

Lean4

noncomputable instance instUnitizationNormedRing : NormedRing (WithLp 1 (Unitization 𝕜 A))
    where
  dist_eq := dist_eq_norm
  norm_mul_le x
    y := by
    simp_rw [unitization_norm_def, add_mul, mul_add, unitization_mul, fst_mul, snd_mul]
    rw [add_assoc, add_assoc]
    gcongr
    · exact norm_mul_le _ _
    · apply (norm_add_le _ _).trans
      gcongr
      · simp [norm_smul]
      · apply (norm_add_le _ _).trans
        gcongr
        · simp [norm_smul, mul_comm]
        · exact norm_mul_le _ _

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