algebraMap_ofSubring

Mathlib.Algebra.Algebra.Basic

URI: https://scilib.ai/kg/mathlib#Algebra.algebraMap_ofSubring

English

The construction provides an algebra over S with the same underlying action restricted to S.

Русский

Конструкция обеспечивает алгебру над S с тем же действием, ограниченным до S.

LaTeX

$$Algebra S A$$

Lean4

theorem algebraMap_ofSubring {R : Type*} [CommRing R] (S : Subring R) :
    (algebraMap S R : S →+* R) = Subring.subtype S :=
  rfl

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

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

Разделы

Аффилиация

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