lof_map_one

Mathlib.LinearAlgebra.FreeProduct.Basic

URI: https://scilib.ai/kg/mathlib#LinearAlgebra.FreeProduct.lof_map_one

English

The lof morphism coincides with the composition of DirectSum.lof and ι'.

Русский

Морфизм lof совпадает по значению с композицией DirectSum.lof и ι'.

LaTeX

$$$\operatorname{lof}_{R,A,i} = (\iota'_{R,A}) \circ (\operatorname{DirectSum.lof}_{R,I,A,i})$$$

Lean4

/-- `lof R A i 1 = 1` for all `i`. -/
theorem lof_map_one (i : I) : lof R A i 1 = 1 := by rw [lof]; dsimp [mkAlgHom]; exact identify_one R A i

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

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

Разделы

Аффилиация

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