Theorems · Theorem · field theory

AlgHom.card_of_powerBasis

∀ {S : Type u_2} [inst : CommRing S] {K : Type u_4} {L : Type u_5} [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra K S] [inst_4 : Algebra K L] (pb : PowerBasis K S),
  IsSeparable K pb.gen → (Polynomial.map (algebraMap K L) (minpoly K pb.gen)).Splits → Fintype.card (S →ₐ[K] L) = pb.dim

Defined in

Mathlib.FieldTheory.Separable

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingFieldFieldAlgebraAlgebra