restrictScalars_symm_apply

Mathlib.Algebra.Algebra.Tower

URI: https://scilib.ai/kg/mathlib#AlgEquiv.restrictScalars_symm_apply

English

Restriction map is injective on AlgEquiv and AlgHom contexts.

Русский

Отображение ограничений инъективно на контекстах AlgEquiv и AlgHom.

LaTeX

$$$\mathrm{restrictScalars}_R\;:\; (A \to_{{S}} B) \to (A \to_{{R}} B)$ инъективно$$

Lean4

theorem restrictScalars_symm_apply (f : A ≃ₐ[S] B) (x : B) : (f.restrictScalars R).symm x = f.symm x :=
  rfl

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

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

Разделы

Аффилиация

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