Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-10 13:12 9feefee8

View on Github →

feat(ring_theory/polynomial): refactor of is_integral_domain_fin (#2119)

  • chore(ring_theory/polynomial): refactor proof of is_noetherian_ring_fin
  • not there yet
  • feat(ring_theory/polynomial): refactor of is_integral_domain_fin
  • fix
  • refactor
  • fix
  • fix
  • suggestion from linter
  • Update src/data/mv_polynomial.lean

Estimated changes