instSubsingleton — Mathlib

English

If K is a subsingleton (i.e., has at most one element) then RatFunc(K) is also a subsingleton. In particular, RatFunc(K) has at most one element whenever K is trivial.

Русский

Если K является единичным ( subsingleton ), то RatFunc(K) тоже является единичным (имеет не более одного элемента).

LaTeX

$$$\text{Subsingleton}(\mathrm{RatFunc}\,K)$$$

Lean4

instance [Subsingleton K] : Subsingleton (RatFunc K) :=
  toFractionRing_injective.subsingleton

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