natDegree_removeFactor — Mathlib

English

The natural degree of the quotient after removing one factor decreases by one: (f.removeFactor).natDegree = f.natDegree − 1.

Русский

Порядковый (натуральный) показатель степени после удаления одного множителя уменьшается на единицу: (f.removeFactor).natDegree = f.natDegree − 1.

LaTeX

$$$\\operatorname{natDegree}(f\\!\\!\\!\\!\\!\\!\\!\\!\\!\\text{removeFactor}) = \\operatorname{natDegree}(f) - 1$$$

Lean4

theorem natDegree_removeFactor (f : K[X]) : f.removeFactor.natDegree = f.natDegree - 1 := by
  rw [removeFactor, natDegree_divByMonic _ (monic_X_sub_C _), natDegree_map, natDegree_X_sub_C]

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