subsingleton — Mathlib

English

If R is a subsingleton (has at most one element) and A is an R-algebra, then A is a subsingleton as well.

Русский

Если R — пододнопорядковое множество (один элемент) и A — алгебра над R, тогда A также пододнопорядковое множество.

LaTeX

$$$[Subsingleton R] \Rightarrow Subsingleton A$ under the given algebraic setup.$$

Lean4

theorem subsingleton (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] [Subsingleton R] :
    Subsingleton A :=
  (algebraMap R A).codomain_trivial

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