ker_copolarization_eq_ker_corootForm

Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear

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

← MathLib Explorer

English

The kernel of CoPolarization equals the kernel of CorootForm: ker P.CoPolarization = ker P.CorootForm.

Русский

Ядро Copolarization равно ядру CorootForm: ker P.CoPolarization = ker P.CorootForm.

LaTeX

$$$ \\ker\\!P.CoPolarization = \\ker\\!P.CorootForm $$$

Lean4

theorem ker_copolarization_eq_ker_corootForm : LinearMap.ker P.CoPolarization = LinearMap.ker P.CorootForm :=
  P.flip.ker_polarization_eq_ker_rootForm

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

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

Разделы

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

Аффилиация

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