domRestrict

Mathlib.LinearAlgebra.SesquilinearForm.Basic

URI: https://scilib.ai/kg/mathlib#LinearMap.IsSymm.domRestrict

← MathLib Explorer

English

Restriction of a symmetric form to a submodule is symmetric.

Русский

Ограничение симметричной формы к подмодулю является симметричным.

LaTeX

$$$\\forall p, (B.domRestrict_{1\\,2} p\\, p).IsSymm$$$

Lean4

theorem domRestrict (H : B.IsSymm) (p : Submodule R M) : (B.domRestrict₁₂ p p).IsSymm where
  eq _
    _ := by
    simp_rw [domRestrict₁₂_apply]
    exact H.eq _ _

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

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

Разделы

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

Аффилиация

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