Theorems · Theorem · commutative algebra

IsCoprime.wronskian_eq_zero_iff

∀ {R : Type u_1} [inst : CommRing R] [NoZeroDivisors R] {a b : Polynomial R},
  IsCoprime a b → (a.wronskian b = 0 ↔ Polynomial.derivative a = 0 ∧ Polynomial.derivative b = 0)

For coprime polynomials a and b, their Wronskian is zero if and only if their derivatives are zeros.

Defined in

Mathlib.RingTheory.Polynomial.Wronskian

Cited by

1 results in Mathlib

Foundations

Depth 111 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingNoZeroDivisors