of_pow — Mathlib

English

If f ∉ IsUnit and f^n is separable with n ≠ 0, then f is separable and n = 1.

Русский

Если f не единица и f^n разделим при n ≠ 0, то f разделим и n = 1.

LaTeX

$$$\\neg \\operatorname{IsUnit}(f) \\land n \\neq 0 \\land (f^n)\\Separable \\Rightarrow (\\operatorname{Separable}(f) \\land n = 1)$$$

Lean4

theorem of_pow {f : R[X]} (hf : ¬IsUnit f) {n : ℕ} (hn : n ≠ 0) (hfs : (f ^ n).Separable) : f.Separable ∧ n = 1 :=
  (hfs.of_pow'.resolve_left hf).resolve_right hn

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