coe_algebraMap

Mathlib.Algebra.DirectSum.Internal

URI: https://scilib.ai/kg/mathlib#SetLike.GradeZero.coe_algebraMap

English

The map algebraMap from S to A(0) followed by the natural inclusion to R coincides with algebraMap from S to R.

Русский

Составные отображения алгебраMap_S→A_0 и включение в R совпадают с алгебраMap_S→R.

LaTeX

$$↑(algebraMap_S^{A_0} s) = algebraMap_S^R s$$

Lean4

@[simp, norm_cast]
theorem coe_algebraMap (s : S) : ↑(algebraMap _ (A 0) s) = algebraMap _ R s :=
  rfl

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

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

Разделы

Аффилиация

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