ker_polarization_eq_ker_rootForm

Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear

URI: https://scilib.ai/kg/mathlib#RootPairing.ker_polarization_eq_ker_rootForm

← MathLib Explorer

English

The kernel of Polarization equals the kernel of RootForm: ker P.Polarization = ker P.RootForm.

Русский

Ядро Polarization равно ядру RootForm: ker P.Polarization = ker P.RootForm.

LaTeX

$$$ \\ker\\!P.Polarization = \\ker\\!P.RootForm $$$

Lean4

theorem ker_polarization_eq_ker_rootForm : LinearMap.ker P.Polarization = LinearMap.ker P.RootForm := by ext;
  simp only [LinearMap.mem_ker, P.polarization_apply_eq_zero_iff]

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

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

Разделы

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

Аффилиация

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