Mathlib v3 is deprecated. Go to Mathlib v4

Def polynomial.degree_lt_equiv

Modification history

2022-05-04 11:10
src/ring_theory/polynomial/basic.lean
fix(ring_theory/polynomial/basic): fix unexpected change of an implicit parameter (#13935) …
Modified polynomial.degree_lt_equivView on Github →
2022-05-03 14:29
src/ring_theory/polynomial/basic.lean
feat(ring_theory/polynomial/basic): reduce assumptions, golf (#13800) …
Modified polynomial.degree_lt_equivView on Github →
2022-04-10 04:05
src/ring_theory/polynomial/basic.lean
chore(ring_theory/polynomial/basic): Generalize `polynomial.degree_lt_equiv` to commutative rings (#13190) …
Modified polynomial.degree_lt_equivView on Github →
2020-10-31 06:18
src/ring_theory/polynomial/basic.lean
feat(ring_theory/polynomial/basic): prerequisites for galois_definition (#4829)
Added polynomial.degree_lt_equivView on Github →