map_comp_mkQ

Mathlib.RingTheory.QuotSMulTop

URI: https://scilib.ai/kg/mathlib#QuotSMulTop.map_comp_mkQ

English

The quotient-map and map commute with mkQ in a linear sense.

Русский

Квази-отображение и отображение коммутируют с mkQ линейным образом.

LaTeX

$$$$ map\_r f \circ mkQ_{r\top} = mkQ_{r\top} \circ f. $$$$

Lean4

theorem map_comp_mkQ (f : M →ₗ[R] M') : map r f ∘ₗ mkQ (r • ⊤) = mkQ (r • ⊤) ∘ₗ f := by ext; rfl

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

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

Разделы

Аффилиация

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