Zulip Chat Archive
Stream: maths
Topic: ring modulo maximal
Johan Commelin (Feb 12 2019 at 10:00):
I guess this should be a discrete_field. Is that right?
https://github.com/leanprover-community/mathlib/blob/9b28db0728954d6566d31fbadbd7b9479bfa6bf8/src/ring_theory/ideals.lean#L325
If so, I'll try to PR it.
Last updated: May 02 2025 at 03:31 UTC