wronskian_eq_of_sum_zero

Mathlib.RingTheory.Polynomial.Wronskian

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

← MathLib Explorer

English

If a + b + c = 0 then W(a,b) = W(b,c).

Русский

Если a + b + c = 0 тогда W(a,b) = W(b,c).

LaTeX

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

Lean4

theorem wronskian_eq_of_sum_zero {a b c : R[X]} (hAdd : a + b + c = 0) : wronskian a b = wronskian b c :=
  isAlt_wronskianBilin.eq_of_add_add_eq_zero hAdd

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

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

Разделы

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

Аффилиация

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