CoPolarizationIn_eq

Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear

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

English

Equality between CoPolarizationIn and the alternative polarization expression holds.

Русский

Справедливость между CoPolarizationIn и альтернативным выражением поляризации сохраняется.

LaTeX

$$$P.CoPolarizationIn S x = P.CoPolarization x$$$

Lean4

theorem CoPolarizationIn_eq (x : P.corootSpan S) : P.CoPolarizationIn S x = P.CoPolarization x :=
  P.flip.PolarizationIn_eq S x

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

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

Разделы

Аффилиация

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