Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-31 06:18 517f0b5c

View on Github →

feat(ring_theory/polynomial/basic): prerequisites for galois_definition (#4829)

Estimated changes

Modified src/data/polynomial/degree/basic.lean

added theorem polynomial.as_sum_range'

Modified src/ring_theory/polynomial/basic.lean

added def polynomial.degree_lt_equiv