Revision #2224 → #2881 · back to history
295dbae7d8ea| Field | From #2224 | To #2881 |
|---|---|---|
| mathlib.decl | — | Polynomial.wronskian |
| mathlib.match_kind | — | special_case |
| mathlib.module | — | Mathlib.RingTheory.Polynomial.Wronskian |
| note | No Wronskian definition was located in Mathlib. | `Polynomial.wronskian a b = a·b' − a'·b` is the two-polynomial Wronskian; the general n-function Wronskian determinant is not formalized. |
| status | not_formalized | partial |
82dbe75b42f560b434620e0947bc383ec88d9f8a0919881786665ba82d2f2aa6cd934958