Theorems · Definition · number theory

FiniteField.algEquivExtension

(k : Type u_1) →
  [inst : Field k] →
    [inst_1 : Finite k] →
      (p : ℕ) →
        [inst_2 : Fact (Nat.Prime p)] →
          [inst_3 : CharP k p] →
            (n : ℕ) →
              [inst_4 : NeZero n] →
                (l : Type u_2) →
                  [inst_5 : Field l] →
                    [inst_6 : Algebra k l] → Module.finrank k l = n → l ≃ₐ[k] FiniteField.Extension k p n

Given any field extension of finite fields l/k of degree n, we have a non-unique isomorphism between l and our chosen Extension k p n.

Defined in

Mathlib.FieldTheory.Finite.Extension

Cited by

3 results in Mathlib

Foundations

Depth 164 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldFiniteFactCharPNeZeroFieldAlgebra