restrictScalars

Mathlib.Algebra.Star.Subalgebra

URI: https://scilib.ai/kg/mathlib#StarAlgHom.restrictScalars

English

Given an injective StarAlgHom f, there is a StarAlgEquiv between A and the range of f.

Русский

С данным инъективным StarAlgHom f существует StarAlgEquiv между A и образцом f.

LaTeX

$$$ \\text{StarAlgEquiv.ofInjective}(f) : A \\simeq⋆_R \\; f.range $$$

Lean4

@[simps!]
def restrictScalars (f : A →⋆ₐ[S] B) : A →⋆ₐ[R] B
    where
  toAlgHom := f.toAlgHom.restrictScalars R
  map_star' := map_star f

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru