Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-28 11:38 fd2c6c47

View on Github →

chore(data/polynomial/ring_division): remove nontrivial assumptions (#12984) Additionally, this removes:

  • some polynomial.monic assumptions that can be handled by casing instead
  • the explicit R argument from is_field.to_field R hR

Estimated changes