natSepDegree_pow_of_ne_zero

Mathlib.FieldTheory.SeparableDegree

URI: https://scilib.ai/kg/mathlib#Polynomial.natSepDegree_pow_of_ne_zero

English

If n ≠ 0, then (f^n).natSepDegree = f.natSepDegree.

Русский

Если n ≠ 0, то (f^n).natSepDegree = f.natSepDegree.

LaTeX

$$$ n \neq 0 \Rightarrow (f^n).\operatorname{natSepDegree} = f.\operatorname{natSepDegree}$$$

Lean4

theorem natSepDegree_pow_of_ne_zero {n : ℕ} (hn : n ≠ 0) : (f ^ n).natSepDegree = f.natSepDegree := by
  simp_rw [natSepDegree_pow, hn, ite_false]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru