is_transcendental_of_subsingleton

English

Let R be a ring with only one element (a subsingleton). For any A which is an R-algebra and any x in A, x is transcendental over R.

Русский

Пусть R — кольцо, содержащее ровно один элемент (Subsingleton). Для любой R-алгебры A и любого элемента x ∈ A, x является трансцендентным над R.

LaTeX

$$$ \forall (R : Type u)\ (A : Type v) [CommRing R] [Ring A] [Algebra R A] [Subsingleton R] (x : A),\ Transcendental R x $$$

Lean4

@[nontriviality]
theorem is_transcendental_of_subsingleton [Subsingleton R] (x : A) : Transcendental R x := fun ⟨p, h, _⟩ =>
  h <| Subsingleton.elim p 0

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