mem_factors_iff_dvd — Mathlib

English

Let a ≠ 0 and p irreducible. Then p appears in the factorization (with Associates) of a if and only if p divides a.

Русский

Пусть a ≠ 0 и p неприводимо. Тогда p встречается в факторизации a по Associates тогда и только тогда, когда p делит a.

LaTeX

$$$$a \\neq 0 \\land \\mathrm{Irreducible}(p) \\Rightarrow \\mathrm{Subtype.mk}(\\mathrm{Associates.mk}p, \\mathrm{irreducible\\_mk}.2\\,hp) \\in \\mathrm{factors}\\,(\\mathrm{Associates.mk}a) \\iff p \\mid a.$$$$

Lean4

theorem mem_factors_iff_dvd {a p : α} (ha0 : a ≠ 0) (hp : Irreducible p) :
    Associates.mk p ∈ factors (Associates.mk a) ↔ p ∣ a :=
  by
  constructor
  · rw [← mk_dvd_mk]
    apply dvd_of_mem_factors
  · apply mem_factors_of_dvd ha0 hp

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