wronskianBilin_apply — Mathlib

English

For any polynomials a and b, the bilinear Wronskian evaluated at a and b coincides with the standard Wronskian of a and b.

Русский

Для любых многочленов a и b применённое к ним bilinear-определение Вронскиана совпадает с обычным Вронскианом a и b.

LaTeX

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

Lean4

@[simp]
theorem wronskianBilin_apply (a b : R[X]) : wronskianBilin R a b = wronskian a b :=
  rfl

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