fieldOfDomain — Mathlib

English

Every finite commutative domain is a field; more generally, commutativity is not required for finite domains to be fields.

Русский

Каждая конечная коммутативная область является полем; в более общем виде финитные области без коммутативности тоже поля.

LaTeX

$$def fieldOfDomain (R) [CommRing R] [IsDomain R] [DecidableEq R] [Fintype R] : Field R$$

Lean4

/-- Every finite commutative domain is a field. More generally, commutativity is not required: this
can be found in `Mathlib/RingTheory/LittleWedderburn.lean`. -/
def fieldOfDomain (R) [CommRing R] [IsDomain R] [DecidableEq R] [Fintype R] : Field R :=
  { Fintype.divisionRingOfIsDomain R, ‹CommRing R› with }

Похожие утверждения