wronskian_neg_left

Mathlib.RingTheory.Polynomial.Wronskian

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

English

Negating the first argument flips the sign: W(−a,b) = −W(a,b).

Русский

Отрицание первого аргумента меняет знак: W(−a,b) = −W(a,b).

LaTeX

$$$$ \\mathrm{wronskian}( -a, b) = -\\mathrm{wronskian}(a,b). $$$$

Lean4

theorem wronskian_neg_left (a b : R[X]) : wronskian (-a) b = -wronskian a b :=
  LinearMap.map_neg₂ (wronskianBilin R) a b

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

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

Разделы

Аффилиация

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