goursatFst_toAddSubgroup

Mathlib.LinearAlgebra.Goursat

URI: https://scilib.ai/kg/mathlib#Submodule.goursatFst_toAddSubgroup

← MathLib Explorer

English

The product of the first and second Goursat components is contained in L.

Русский

Произведение первых компонент Гурсата содержится в L.

LaTeX

$$$ L.goursatFst.prod L.goursatSnd \leq L $$$

Lean4

theorem goursatFst_toAddSubgroup : (goursatFst L).toAddSubgroup = L.toAddSubgroup.goursatFst :=
  by
  ext x
  simp [mem_toAddSubgroup, goursatFst, AddSubgroup.mem_goursatFst]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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