isAlt_wronskianBilin

Mathlib.RingTheory.Polynomial.Wronskian

URI: https://scilib.ai/kg/mathlib#Polynomial.isAlt_wronskianBilin

English

The Wronskian bilinear form is alternating: its diagonal vanishes, i.e., W(a,a) = 0 for all a.

Русский

Билинейная форма Вронскиана чередуется: на диагонали ноль, то есть W(a,a) = 0 для всех a.

LaTeX

$$$$ (\\mathrm{wronskianBilin}\\, R).\\mathrm{IsAlt} $$$$

Lean4

theorem isAlt_wronskianBilin : (wronskianBilin R).IsAlt :=
  wronskian_self_eq_zero

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

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

Разделы

Аффилиация

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