factors_subsingleton — Mathlib

English

If α is a subsingleton, then for every a in Associates α, a.factors = ⊤.

Русский

Если α — пододносуждающее множество, то для любого a ∈ Associates α, a.factors = ⊤.

LaTeX

$$[Subsingleton α] {a : Associates α} : a.factors = ⊤$$

Lean4

@[nontriviality]
theorem factors_subsingleton [Subsingleton α] {a : Associates α} : a.factors = ⊤ :=
  by
  have : Subsingleton (Associates α) := inferInstance
  convert factors_zero

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