Theorems · Theorem · field theory

AlgHom.card

∀ (F : Type u_1) (E : Type u_2) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E]
  [inst_3 : FiniteDimensional F E] [Algebra.IsSeparable F E] (K : Type u_3) [inst_5 : Field K] [IsAlgClosed K]
  [inst_7 : Algebra F K], Fintype.card (E →ₐ[F] K) = Module.finrank F E

Defined in: Mathlib.FieldTheory.PrimitiveElement
Cited by: 10 results in Mathlib
Foundations: Depth 160 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Field Field Algebra FiniteDimensional Algebra.IsSeparable Field IsAlgClosed Algebra

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites13

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
Algebra.algebraMapproof · cited by 4,706
AlgHomstatement · cited by 3,236
FiniteDimensionalstatement and proof · cited by 1,854
Module.finrankstatement · cited by 1,770
Fintype.cardstatement · cited by 1,386
Polynomial.mapproof · cited by 806
minpolyproof · cited by 439
Algebra.IsSeparablestatement and proof · cited by 210
IsAlgClosedstatement and proof · cited by 150
IsAlgClosed.splitsproof · cited by 29

Cited by10

Results whose statement or proof uses this declaration.

NumberField.Embeddings.cardproof · cited by 6
IsPrimitiveRoot.sub_one_norm_eq_eval_cyclotomicproof · cited by 3
det_traceMatrix_ne_zero'proof · cited by 1
NumberField.InfinitePlace.unramifedPlacesOver_ncard_add_eq_finrankproof · cited by 1
sum_smul_minpolyDiv_eq_X_powproof · cited by 1
Algebra.discr_powerBasis_eq_normproof · cited by 1
Algebra.discr_powerBasis_eq_prod''proof · cited by 1
sum_embeddings_eq_finrank_mulproof · cited by 1
Algebra.prod_embeddings_eq_finrank_powproof · cited by 1
NumberField.norm_norm_le_norm_mul_house_powproof · cited by 0