trunc_trunc_pow — Mathlib

English

For any f and a ∈ N, trunc n ((trunc n f)^a) = trunc n (f^a).

Русский

Для любого f и a ∈ N: trunc n ((trunc n f)^a) = trunc n (f^a).

LaTeX

$$$\\forall f:\\; \\mathbb{R}\\langle\\langle X \\rangle\\rangle, \\forall a \\in \\mathbb{N}, \\; \\operatorname{trunc} n ((\\operatorname{trunc} n f)^a) = \\operatorname{trunc} n (f^a)$$$

Lean4

@[simp]
theorem trunc_trunc_pow (f : R⟦X⟧) (n a : ℕ) : trunc n ((trunc n f : R⟦X⟧) ^ a) = trunc n (f ^ a) := by
  induction a with
  | zero => rw [pow_zero, pow_zero]
  | succ a ih =>
    rw [_root_.pow_succ', _root_.pow_succ', trunc_trunc_mul, ← trunc_trunc_mul_trunc, ih, trunc_trunc_mul_trunc]

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