emultiplicity_le_one_of_separable

English

If q is not a unit and p is separable, then the emultiplicity of q in p is at most 1.

Русский

Если q не единица и p разделим, то эм-умножимость q в p не превышает 1.

LaTeX

$$$\\neg \\operatorname{IsUnit}(q) \\land \\operatorname{Separable}(p) \\Rightarrow emultiplicity(q,p) \\le 1$$$

Lean4

theorem emultiplicity_le_one_of_separable {p q : R[X]} (hq : ¬IsUnit q) (hsep : Separable p) : emultiplicity q p ≤ 1 :=
  by
  contrapose! hq
  apply isUnit_of_self_mul_dvd_separable hsep
  rw [← sq]
  apply pow_dvd_of_le_emultiplicity
  exact Order.add_one_le_of_lt hq

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