factors_self — Mathlib

English

For a irreducible p, the factor multiset of p is a singleton consisting of p itself (as an associated class).

Русский

Для неприводимого p множество его факторов состоит из одного элемента — самого p (как ассоциированного класса).

LaTeX

$$$$\\text{If } hp = \\mathrm{Irreducible}(p),\\, p\\!\\in\\mathrm{factors}\\\\(p) = \\mathrm{WithTop}.\\mathrm{some}\\, \\{\\langle p, hp \\rangle\\}.$$$$

Lean4

theorem factors_self [Nontrivial α] {p : Associates α} (hp : Irreducible p) : p.factors = WithTop.some {⟨p, hp⟩} :=
  FactorSet.unique (by rw [factors_prod, FactorSet.prod.eq_def]; dsimp; rw [prod_singleton])

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