English
Every finite domain is a division ring; more generally, finite division rings are fields.
Русский
Каждая конечная область является дивизионным кольцом; более общо конечные дивизионные кольца являются полями.
LaTeX
$$def divisionRingOfIsDomain (R) [Ring R] [IsDomain R] [DecidableEq R] [Fintype R] : DivisionRing R$$
Lean4
/-- Every finite domain is a division ring. More generally, they are fields; this can be found in
`Mathlib/RingTheory/LittleWedderburn.lean`. -/
def divisionRingOfIsDomain (R : Type*) [Ring R] [IsDomain R] [DecidableEq R] [Fintype R] : DivisionRing R
where
__ :=
(‹Ring R› :) -- this also works without the `( :)`, but it's slightly slow
__ := Fintype.groupWithZeroOfCancel R
nnqsmul := _
nnqsmul_def := fun _ _ => rfl
qsmul := _
qsmul_def := fun _ _ => rfl
