X_pow_card_pow_sub_X_natDegree_eq

English

If n ≠ 0 and p > 1, then the natDegree of X^{p^n} − X over K' is p^n.

Русский

Если n ≠ 0 и p > 1, то степенность natDegree многочлена X^{p^n} − X над K' равна p^n.

LaTeX

$$$(\\text{hn} : n \\neq 0) \\land (\\text{hp} : 1 < p) \\Rightarrow \\operatorname{natDegree}\\left(X^{p^n} - X\\right) = p^n$$$

Lean4

theorem X_pow_card_pow_sub_X_natDegree_eq (hn : n ≠ 0) (hp : 1 < p) : (X ^ p ^ n - X : K'[X]).natDegree = p ^ n :=
  X_pow_card_sub_X_natDegree_eq K' <| Nat.one_lt_pow hn hp

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