Finite.isDomain_to_isField

theorem Finite.isDomain_to_isField : ∀ (D : Type u_1) [inst : Finite D] [inst : Ring D] [inst_1 : IsDomain D], IsField D

The theorem `Finite.isDomain_to_isField` states that for any type `D` that is a finite set and has the structure of a ring and a domain, `D` also has the structure of a field. This means that within the constraints defined by the `Finite`, `Ring`, and `IsDomain` typeclasses, every non-zero element in `D` has a multiplicative inverse, which is a defining property of a field. See also the theorems `littleWedderburn` and `Fintype.divisionRingOfIsDomain` for related concepts.

More concisely: A finite ring and a domain is a field. Every non-zero element in such a finite field has a multiplicative inverse.