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