algebraMap_eq_inl'

Mathlib.Algebra.TrivSqZeroExt

URI: https://scilib.ai/kg/mathlib#TrivSqZeroExt.algebraMap_eq_inl'

English

TrivSqZeroExt carries a canonical algebra structure over S, built from the left and right injections.

Русский

TrivSqZeroExt имеет каноническую структуру алгебры над S, построенную из l-inl и inr.

LaTeX

$$$ \\exists \\mathcal{A} : Algebra S (tsze R M) \\; \\text{with the maps given by } inl, inr $$$

Lean4

theorem algebraMap_eq_inl' (s : S) : algebraMap S (tsze R M) s = inl (algebraMap S R s) :=
  rfl

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

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

Разделы

Аффилиация

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