subsingleton_iff — Mathlib

English

The power series ring R⟦X⟧ is a singleton if and only if R is a singleton; equivalently, Subsingleton(R⟦X⟧) ⇔ Subsingleton(R).

Русский

Кольцо степенных рядов над R имеет не более одного элемента тогда и только тогда, когда R имеет не более одного элемента.

LaTeX

$$$\operatorname{Subsingleton}(R⟦X⟧)\;\iff\;\operatorname{Subsingleton}(R)$$$

Lean4

protected theorem subsingleton_iff : Subsingleton R⟦X⟧ ↔ Subsingleton R :=
  by
  refine ⟨fun h ↦ ?_, fun _ ↦ inferInstance⟩
  rw [subsingleton_iff] at h ⊢
  exact fun a b ↦ C_injective (h (C a) (C b))

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