mathlib

4089712f - chore(ring_theory/polynomial): refactor proof of is_noetherian_ring_fin (#2117)