fieldOfFiniteDimensional — Mathlib

English

Let F be a field and K a finite-dimensional F-algebra that is a domain. Then every nonzero element of K is a unit.

Русский

Пусть F — поле, K — конечномерная F-алгебра и интегральный домен. Тогда любой ненулевой элемент K является едичкой (обратим).

LaTeX

$$$\text{Nonzero } x \in K \Rightarrow \text{IsUnit } x$$$

Lean4

/-- An integral domain that is module-finite as an algebra over a field is a field. -/
noncomputable def fieldOfFiniteDimensional (F K : Type*) [Field F] [h : CommRing K] [IsDomain K] [Algebra F K]
    [FiniteDimensional F K] : Field K :=
  { divisionRingOfFiniteDimensional F K with toCommRing := h }

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