mem_factorSet_top — Mathlib

English

If p is irreducible in the Associates α, then p lies in the top element of the FactorSet α.

Русский

Если p неприводим в группе Ассоциатов α, то он принадлежит верхнему элементу FactorSet α.

LaTeX

$$$p \\in (\\top : \\mathrm{FactorSet}(\\alpha))$$$

Lean4

theorem mem_factorSet_top {p : Associates α} {hp : Irreducible p} : p ∈ (⊤ : FactorSet α) := by
  dsimp only [Membership.mem]; dsimp only [FactorSetMem]; split_ifs; exact trivial

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