natSepDegree_mul — Mathlib

English

For polynomials f and g over F, the separable degree of their product is at most the sum of their separable degrees.

Русский

Для многочленов f и g над F разделяемая степень их произведения не превосходит суммы их разделяемых степеней.

LaTeX

$$$ (f \cdot g).\operatorname{natSepDegree} \leq f.\operatorname{natSepDegree} + g.\operatorname{natSepDegree}$$$

Lean4

theorem natSepDegree_mul (g : F[X]) : (f * g).natSepDegree ≤ f.natSepDegree + g.natSepDegree :=
  by
  by_cases h : f * g = 0
  · simp only [h, natSepDegree_zero, zero_le]
  classical
  simp_rw [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F), aroots_mul h, Multiset.toFinset_add]
  exact Finset.card_union_le _ _

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