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

added theorem is_field.nontrivial
modified theorem polynomial.not_is_field
modified theorem polynomial.add_mod_by_monic
modified theorem adjoin_root.mk_left_inverse
modified theorem adjoin_root.mk_surjective