mem_factors_of_dvd — Mathlib

English

If a ≠ 0 and p is irreducible and p divides a, then the class of p appears among the factors of the class of a.

Русский

Если a ≠ 0 и p неприводимо и p делит a, то класс p входит в множество факторов класса a.

LaTeX

$$$$a \\neq 0 \\land \\mathrm{Irreducible}(p) \\land p \\mid a \\Rightarrow \\mathrm{Associates.mk}p \\in \\mathrm{factors}\\, (\\mathrm{Associates.mk}a).$$$$

Lean4

theorem mem_factors_of_dvd {a p : α} (ha0 : a ≠ 0) (hp : Irreducible p) (hd : p ∣ a) :
    Associates.mk p ∈ factors (Associates.mk a) :=
  by
  rw [factors_mk _ ha0]
  exact mem_factorSet_some.mpr (mem_factors'_of_dvd ha0 hp hd)

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