instUniqueAlgEquivOfSubsingleton — Mathlib

English

Every Group element defines an algebra equivalence; thus toAlgEquiv maps G to AlgEquiv_R(A,A).

Русский

Каждый элемент группы задаёт алгебраическое эквивалентное отображение; следовательно toAlgEquiv отображает G в AlgEquiv_R(A,A).

LaTeX

$$$ g \\mapsto (A \\overset{toAlgEquiv}{\\cong} A) \\,\\; \\text{R-алгеб. эквив авт.} $$$

Lean4

instance [Subsingleton S] [Subsingleton T] : Unique (S ≃ₐ[R] T)
    where
  default :=
    AlgEquiv.ofAlgHom default default (AlgHom.ext fun _ ↦ Subsingleton.elim _ _)
      (AlgHom.ext fun _ ↦ Subsingleton.elim _ _)
  uniq _ := AlgEquiv.ext fun _ ↦ Subsingleton.elim _ _

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