natSepDegree_mul_of_isCoprime — Mathlib

English

If f and g are coprime, then the separable degree of their product equals the sum of their separable degrees.

Русский

Если f и g взаимно просты, то разделяемая степень их произведения равна сумме разделяемых степеней.

LaTeX

$$$ IsCoprime f g \Rightarrow (f \cdot g).natSepDegree = f.natSepDegree + g.natSepDegree $$$

Lean4

theorem natSepDegree_mul_of_isCoprime (g : F[X]) (hc : IsCoprime f g) :
    (f * g).natSepDegree = f.natSepDegree + g.natSepDegree :=
  (natSepDegree_mul_eq_iff f g).2 (.inr hc)

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