of_subsingleton — Mathlib

English

If R is a subsingleton, then x is algebraically independent over R.

Русский

Пусть R — коммутативное кольцо, A — R-алгебра, x: ι → A. Если R является подмножество одного элемента, то множество x алгебраически независимо над R.

LaTeX

$$$\\operatorname{AlgIndep}_R(x)$$$

Lean4

@[nontriviality]
theorem of_subsingleton [Subsingleton R] : AlgebraicIndependent R x :=
  algebraicIndependent_iff.2 fun _ _ => Subsingleton.elim _ _

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