wronskian_self_eq_zero

Mathlib.RingTheory.Polynomial.Wronskian

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

English

The Wronskian of a with itself is zero: W(a,a) = 0.

Русский

Вронскиан для одинаковых аргументов равен нулю: W(a,a) = 0.

LaTeX

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

Lean4

theorem wronskian_self_eq_zero (a : R[X]) : wronskian a a = 0 := by rw [wronskian, mul_comm, sub_self]

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

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

Разделы

Аффилиация

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