Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-06 22:46 e00d6e08

View on Github →

feat(data/polynomial/*): Specific root sets (#7510) Adds lemmas for the root sets of a couple specific polynomials.

Estimated changes

Modified src/data/polynomial/field_division.lean

added theorem polynomial.root_set_C_mul_X_pow

added theorem polynomial.root_set_X_pow

added theorem polynomial.root_set_monomial

Modified src/data/polynomial/ring_division.lean

added theorem polynomial.root_set_C