subsingleton_iff_subsingleton — Mathlib

English

The polynomial ring R[X] is a singleton if and only if R is a singleton.

Русский

Кольцо полиномов R[X] является одноэлементным тогда и только тогда, когда R также одноэлементно.

LaTeX

$$$\operatorname{Subsingleton}(R[X]) \iff \operatorname{Subsingleton}(R)$$$

Lean4

theorem subsingleton_iff_subsingleton : Subsingleton R[X] ↔ Subsingleton R :=
  ⟨@Injective.subsingleton _ _ _ C_injective, by
    intro
    infer_instance⟩

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