Theorems · Definition · linear algebra

divisionRingOfFiniteDimensional

(F : Type u_1) →
  (K : Type u_2) →
    [inst : Field F] →
      [inst_1 : Ring K] → [IsDomain K] → [inst_3 : Algebra F K] → [FiniteDimensional F K] → DivisionRing K

A domain that is module-finite as an algebra over a field is a division ring.

Defined in: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Cited by: 2 results in Mathlib
Foundations: Depth 123 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Field Ring IsDomain Algebra FiniteDimensional

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites8

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Algebrastatement and proof · cited by 11,388
Ringstatement and proof · cited by 7,463
Fieldstatement and proof · cited by 7,404
IsDomainstatement and proof · cited by 2,196
FiniteDimensionalstatement and proof · cited by 1,854
DivisionRingstatement · cited by 1,062
NNRatproof · cited by 523
NNRat.castproof · cited by 235

Cited by3

Results whose statement or proof uses this declaration.

FiniteDimensional.isUnitproof · cited by 1
fieldOfFiniteDimensionalproof · cited by 1
Subalgebra.isSimpleOrder_of_finrank_primeproof · cited by 0