instSubsingletonQuaternion — Mathlib

English

If the base ring R is subsingleton, then the quaternion algebra ℍ(R) is subsingleton as a type.

Русский

Если база R имеет единственный элемент, то ℍ(R) тоже является вырожденным типом (один элемент).

LaTeX

$$$$ \text{If } \#R = 1, \text{ then } \#\mathbb{H}(R) = 1.$$$$

Lean4

instance {R : Type*} [Zero R] [One R] [Neg R] [Subsingleton R] : Subsingleton ℍ[R] :=
  inferInstanceAs (Subsingleton <| ℍ[R,-1,0,-1])

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