trunc_mul_trunc — Mathlib

English

Truncation of the product of truncated series equals truncation of the full product: trunc n (trunc n f · trunc n g) = trunc n (f · g).

Русский

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

LaTeX

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

Lean4

@[simp]
theorem trunc_mul_trunc {n} (f g : R⟦X⟧) : trunc n (f * (trunc n g) : R⟦X⟧) = trunc n (f * g) := by
  rw [mul_comm, trunc_trunc_mul, mul_comm]

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