subsingleton_right — Mathlib

English

If Subalgebra R B is singleton, then AlgEquiv R A B is a subsingleton.

Русский

Если Subalgebra R B одноэлементна, то AlgEquiv R A B единична.

LaTeX

$$$ \\mathrm{AlgEquiv.subsingleton_right} : [\\mathrm{Subsingleton} (\\mathrm{Subalgebra} R B)] \\Rightarrow \\mathrm{Subsingleton} (A \\simeq_{R} B) $$$

Lean4

instance _root_.AlgEquiv.subsingleton_right [Subsingleton (Subalgebra R B)] : Subsingleton (A ≃ₐ[R] B) :=
  ⟨fun f g => by rw [← f.symm_symm, Subsingleton.elim f.symm g.symm, g.symm_symm]⟩

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