Theorems · Theorem · number theory

FiniteField.card_algHom_of_finrank_dvd

∀ {F : Type u_3} {K : Type u_4} {L : Type u_5} [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra F K]
  [inst_3 : Field L] [inst_4 : Algebra F L] [Finite L] [inst_6 : Finite K],
  Module.finrank F K ∣ Module.finrank F L → Fintype.card (K →ₐ[F] L) = Module.finrank F K

Defined in: Mathlib.FieldTheory.Finite.GaloisField
Cited by: 0 results in Mathlib
Foundations: Depth 200 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Field Field Algebra Field Algebra Finite Finite

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
Fieldstatement and proof · cited by 7,404
AlgHomstatement · cited by 3,236
Finitestatement and proof · cited by 3,029
Module.finrankstatement and proof · cited by 1,770
Fintype.cardstatement · cited by 1,386
Fintype.card_eq_nat_cardproof · cited by 31
FiniteField.natCard_algHom_of_finrank_dvdproof · cited by 1

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.