littleWedderburn — Mathlib

English

A finite division ring is a field.

Русский

Конечное деление кольца является полем.

LaTeX

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

Lean4

/-- A finite division ring is a field. See `Finite.isDomain_to_isField` and
`Fintype.divisionRingOfIsDomain` for more general statements, but these create data, and therefore
may cause diamonds if used improperly. -/
instance (priority := 100) littleWedderburn (D : Type*) [DivisionRing D] [Finite D] : Field D :=
  { ‹DivisionRing D› with mul_comm := fun x y ↦ by simp [Subring.mem_center_iff.mp ?_ x, center_eq_top D] }

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