Commit 2021-10-20 19:43 8366f932
View on Github →feat(ring_theory/integral_domain): finite domains are division rings (#9823) TODO: Prove Wedderburn's little theorem which shows a finite domain is in fact commutative, hence a field.
feat(ring_theory/integral_domain): finite domains are division rings (#9823) TODO: Prove Wedderburn's little theorem which shows a finite domain is in fact commutative, hence a field.