Commit 2022-03-01 19:12 818c81fc

View on Github →

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.

Estimated changes