isDomain_to_isField — Mathlib

English

A finite domain is a field.

Русский

Конечное доменное кольцо — это поле.

LaTeX

$$$\\operatorname{IsField}(D)$$$

Lean4

/-- A finite domain is a field. See also `littleWedderburn` and `Fintype.divisionRingOfIsDomain`. -/
theorem isDomain_to_isField (D : Type*) [Finite D] [Ring D] [IsDomain D] : IsField D := by
  classical
  cases nonempty_fintype D
  let _ := Fintype.divisionRingOfIsDomain D
  let _ := littleWedderburn D
  exact Field.toIsField D

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