splits_pow — Mathlib

English

If f ∈ K[X] splits via i, then f^n splits via i for every natural number n.

Русский

Если полином f ∈ K[X] раскладывается через i, то и f^n раскладывается через i для любого натурального n.

LaTeX

$$$\text{If } f \text{ splits via } i, \ \, \forall n \in \mathbb{N},\ (f^n) \text{ splits via } i$$$

Lean4

theorem splits_pow {f : K[X]} (hf : f.Splits i) (n : ℕ) : (f ^ n).Splits i :=
  by
  rw [← Finset.card_range n, ← Finset.prod_const]
  exact splits_prod i fun j _ => hf

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