Theorems · Theorem · number theory

FiniteField.finrank_zmod_extension

∀ (k : Type u_1) [inst : Field k] [Finite k] (p : ℕ) [inst_2 : Fact (Nat.Prime p)] [inst_3 : CharP k p] (n : ℕ)
  [NeZero n] [inst_5 : Algebra (ZMod p) k],
  Module.finrank (ZMod p) (FiniteField.Extension k p n) = Module.finrank (ZMod p) k * n

Defined in

Mathlib.FieldTheory.Finite.Extension

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldFiniteFactCharPNeZeroAlgebra