of_subsingleton — Mathlib

English

If R is a subsingleton and ι is nonempty, then IsTranscendenceBasis R x.

Русский

Если R — подмножество одного элемента и ι непусто, то x является трансцендентной базой над R.

LaTeX

$$$[\\text{Subsingleton }R] [\\text{Nonempty }\\iota] \\Rightarrow \\mathrm{IsTB}_R(x)$$$

Lean4

@[nontriviality]
theorem of_subsingleton [Subsingleton R] [Nonempty ι] : IsTranscendenceBasis R x :=
  (isTranscendenceBasis_iff_of_subsingleton x).mpr ‹_›

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