mathlib

818c81fc - feat(ring_theory/integral_domain): finite integral domain is a field (#12376)

feat(ring_theory/integral_domain): finite integral domain is a field (#12376) We don't yet have Wedderburn's little theorem (on my todo list), so adding some weaker versions to tide us over.