English
The norm is multiplicative: (f · g).norm = f.norm · g.norm.
Русский
Норма умножения (нормa последовательности) равна произведению норм: (f·g).norm = f.norm · g.norm.
LaTeX
$$$(f \cdot g).norm = f.norm \cdot g.norm$$$
Lean4
theorem norm_mul (f g : PadicSeq p) : (f * g).norm = f.norm * g.norm := by
classical
exact
if hf : f ≈ 0 then by
have hg : f * g ≈ 0 := mul_equiv_zero' _ hf
simp only [hf, hg, norm, dif_pos, zero_mul]
else
if hg : g ≈ 0 then by
have hf : f * g ≈ 0 := mul_equiv_zero _ hg
simp only [hf, hg, norm, dif_pos, mul_zero]
else by
unfold norm
have hfg := mul_not_equiv_zero hf hg
simp only [hfg, hf, hg, dite_false]
-- Porting note: originally `padic_index_simp [hfg, hf, hg]`
rw [lift_index_left_left hfg, lift_index_left hf, lift_index_right hg]
apply padicNorm.mul
