dvd_of_mem_factors — Mathlib

English

If p is in the factors of a, then p divides a.

Русский

Если p лежит в факторах a, то p делит a.

LaTeX

$$hm : p ∈ factors a → p ∣ a$$

Lean4

theorem dvd_of_mem_factors {a p : Associates α} (hm : p ∈ factors a) : p ∣ a :=
  by
  rcases eq_or_ne a 0 with rfl | ha0
  · exact dvd_zero p
  obtain ⟨a0, nza, ha'⟩ := exists_non_zero_rep ha0
  rw [← Associates.factors_prod a]
  rw [← ha', factors_mk a0 nza] at hm ⊢
  rw [prod_coe]
  apply Multiset.dvd_prod; apply Multiset.mem_map.mpr
  exact ⟨⟨p, irreducible_of_mem_factorSet hm⟩, mem_factorSet_some.mp hm, rfl⟩

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