English
A domain that is a finite-dimensional algebra over a field is a division ring (and, when the base ring is commutative, a field).
Русский
Домен, являющийся конечномерной алгеброй над полем, является делением кольца; в случае коммутативности основания — полем.
LaTeX
$$$\operatorname{FiniteDimensional} F K \land \operatorname{IsDomain} K \Rightarrow \text{Field } K$$$
Lean4
/-- A domain that is module-finite as an algebra over a field is a division ring. -/
noncomputable def divisionRingOfFiniteDimensional (F K : Type*) [Field F] [Ring K] [IsDomain K] [Algebra F K]
[FiniteDimensional F K] : DivisionRing K where
__ := ‹IsDomain K›
inv
x :=
letI := Classical.decEq K
if H : x = 0 then 0 else Classical.choose <| FiniteDimensional.exists_mul_eq_one F H
mul_inv_cancel x
hx :=
show x * dite _ (h := _) _ _ = _ by
rw [dif_neg hx]
exact (Classical.choose_spec (FiniteDimensional.exists_mul_eq_one F hx) :)
inv_zero := dif_pos rfl
nnqsmul := _
nnqsmul_def := fun _ _ => rfl
qsmul := _
qsmul_def := fun _ _ => rfl
