Theorems · Theorem · number theory

FiniteField.orderOf_frobeniusAlgHom

∀ (K : Type u_1) [inst : Field K] [inst_1 : Fintype K] (L : Type u_3) [inst_2 : Field L] [inst_3 : Algebra K L]
  [Finite L], orderOf (FiniteField.frobeniusAlgHom K L) = Module.finrank K L

Defined in

Mathlib.FieldTheory.Finite.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

FieldFintypeFieldAlgebraFinite