Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-03 14:29 36b5341d

View on Github →

feat(ring_theory/polynomial/basic): reduce assumptions, golf (#13800) There is some reorder, so the diff is a bit large. Sorry for that.

Estimated changes

Modified src/ring_theory/polynomial/basic.lean

modified theorem ideal.is_fg_degree_le

modified def polynomial.degree_lt_equiv

modified theorem polynomial.map_restriction

modified theorem polynomial.monic.geom_sum'

modified theorem polynomial.monic.geom_sum

modified theorem polynomial.monic_geom_sum_X