natSepDegree_le_of_dvd — Mathlib

English

If f divides g and g ≠ 0, then f.natSepDegree ≤ g.natSepDegree.

Русский

Если f делит g и g ≠ 0, то f.natSepDegree ≤ g.natSepDegree.

LaTeX

$$$ f \mid g \ && g \neq 0 \Rightarrow f.natSepDegree \le g.natSepDegree $$$

Lean4

theorem natSepDegree_le_of_dvd (g : F[X]) (h1 : f ∣ g) (h2 : g ≠ 0) : f.natSepDegree ≤ g.natSepDegree := by
  classical
  simp_rw [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F)]
  exact
    Finset.card_le_card <|
      Multiset.toFinset_subset.mpr <| Multiset.Le.subset <| roots.le_of_dvd (map_ne_zero h2) <| map_dvd _ h1

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