Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-21 11:25 2a1e571f

View on Github →

chore(data/polynomial/basic): golf (#17656) Add polynomial.C_injective, golf some proofs

Estimated changes

modified theorem polynomial.C_eq_zero
modified theorem polynomial.C_inj
added theorem polynomial.C_injective