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.
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.