Commit 2023-12-13 16:04 4275e9e1

View on Github →

feat: Wedderburn's Little Theorem (#6800)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/IntegralDomain.lean

Created Mathlib/RingTheory/LittleWedderburn.lean

added theorem Finite.isDomain_to_isField

Modified Mathlib/RingTheory/Subring/Basic.lean

added theorem Subring.card_top

Modified docs/references.bib