feat: IsCoprime.wronskian_eq_zero_iff

[seewoo5]

---

Add IsCoprime.wronskian_eq_zero_iff: For two polynomials $a, b \in k[x]$ over a field, $W(a, b) = 0$ if and only if $a' = b' = 0$. This is a part of PR #15706.

[github-actions]

PR summary 3ffea3b555

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.Polynomial.Wronskian	980	981	+1 (+0.10%)

Import changes for all files

Files	Import difference
Mathlib.RingTheory.Polynomial.Wronskian	1

---

Declarations diff

+ IsCoprime.wronskian_eq_zero_iff
+ dvd_derivative_iff

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.