instNontrivial — Mathlib

English

If K is a nontrivial commutative ring, then RatFunc(K) is nontrivial as a ring. In particular, RatFunc(K) contains at least two distinct elements when K is not the trivial ring.

Русский

Если K не тривиально как коммутативное кольцо, то RatFunc(K) также не тривиально, то есть содержит не менее двух различных элементов.

LaTeX

$$$\mathrm{Nontrivial}\bigl(\mathrm{RatFunc}\,K\bigr)$$$

Lean4

instance instNontrivial [Nontrivial K] : Nontrivial (RatFunc K) :=
  ofFractionRing_injective.nontrivial

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