factors_one — Mathlib

English

Let a ≠ 0 and hp irreducible. Then Subtype.mk (Associates.mk p) (irreducible_mk.2 hp) ∈ factors' a iff p ∣ a.

Русский

Пусть a ≠ 0 и p неприводимо. Тогда Subtype.mk(Associates.mk p, irreducible_mk.2 hp) ∈ factors' a тогда и только тогда, когда p делит a.

LaTeX

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

Lean4

@[simp]
theorem factors_one [Nontrivial α] : factors (1 : Associates α) = 0 :=
  by
  apply FactorSet.unique
  rw [Associates.factors_prod]
  exact Multiset.prod_zero

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