wronskian_add_left

Mathlib.RingTheory.Polynomial.Wronskian

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

English

Wronskian is linear in the first argument: W(a+b,c) = W(a,c) + W(b,c).

Русский

Wronskian линейна по первому аргументу: W(a+b,c) = W(a,c) + W(b,c).

LaTeX

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

Lean4

theorem wronskian_add_left (a b c : R[X]) : wronskian (a + b) c = wronskian a c + wronskian b c :=
  (wronskianBilin R).map_add₂ a b c

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

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

Разделы

Аффилиация

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