wronskian

Mathlib.RingTheory.Polynomial.Wronskian

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

Lean4

/-- Wronskian of a pair of polynomials, `W(a, b) = ab' - a'b`. -/
def wronskian (a b : R[X]) : R[X] :=
  a * (derivative b) - (derivative a) * b

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

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

Разделы

Аффилиация

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