trunc_trunc_mul — Mathlib

English

Truncation distributes over multiplication with the right factor kept intact: trunc n ((trunc n f) · g) = trunc n (f · g).

Русский

Усечение распадается на произведение слева с сохранением правого множителя: trunc n ((trunc n f) · g) = trunc n (f · g).

LaTeX

$$$\\forall n, f, g:\\; \\operatorname{trunc} n ((\\operatorname{trunc} n f) \\cdot g) = \\operatorname{trunc} n (f \\cdot g)$$$

Lean4

@[simp]
theorem trunc_trunc_mul {n} (f g : R⟦X⟧) : trunc n ((trunc n f) * g : R⟦X⟧) = trunc n (f * g) :=
  by
  ext m
  rw [coeff_trunc, coeff_trunc]
  split_ifs with h
  · rw [coeff_mul, coeff_mul, sum_congr rfl]
    intro _ hab
    have ha := lt_of_le_of_lt (antidiagonal.fst_le hab) h
    rw [coeff_coe, coeff_trunc, if_pos ha]
  · rfl

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