algebraMap_eq_inl

Mathlib.Algebra.Algebra.Unitization

URI: https://scilib.ai/kg/mathlib#Unitization.algebraMap_eq_inl

English

Inl and algebra maps commute up to structural compatibility in Unitization.

Русский

Inl и алгебра Map коммутируют с учётом структуры Unitization.

LaTeX

$$$[\mathrm{fstHom}, \mathrm{inlRingHom}] = 0$ in appropriate sense.$$

Lean4

theorem algebraMap_eq_inl : ⇑(algebraMap R (Unitization R A)) = inl :=
  rfl

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

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

Разделы

Аффилиация

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