English
The L1-based seminorm structure on tsze R M is inherited from the product seminorm.
Русский
Структура нормирования L1 на tsze R M наследуется от произведения норм.
LaTeX
$$$\\text{instL1SeminormedRing} \\Rightarrow \\text{norm on } tsze(R,M) \\text{ is } \\|\\cdot\\| = \\|\\mathrm{fst}(\\cdot)\\| + \\|\\mathrm{snd}(\\cdot)\\|$$$
Lean4
instance instL1SeminormedRing : SeminormedRing (tsze R M)
where
norm_mul_le
| ⟨r₁, m₁⟩, ⟨r₂, m₂⟩ => by
simp_rw [norm_def]
calc
‖r₁ * r₂‖ + ‖r₁ • m₂ + MulOpposite.op r₂ • m₁‖
_ ≤ ‖r₁‖ * ‖r₂‖ + (‖r₁‖ * ‖m₂‖ + ‖r₂‖ * ‖m₁‖) := by
gcongr
· apply norm_mul_le
· refine norm_add_le_of_le ?_ ?_ <;> apply norm_smul_le
_ ≤ ‖r₁‖ * ‖r₂‖ + (‖r₁‖ * ‖m₂‖ + ‖r₂‖ * ‖m₁‖) + (‖m₁‖ * ‖m₂‖) :=
by
apply le_add_of_nonneg_right
positivity
_ = (‖r₁‖ + ‖m₁‖) * (‖r₂‖ + ‖m₂‖) := by ring
__ : SeminormedAddCommGroup (tsze R M) := inferInstance
__ : Ring (tsze R M) := inferInstance
