Theorems · Theorem · field theory
AlgHom.card_of_splits
∀ (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] (L : Type u_3) [inst_5 : Field L] [inst_6 : Algebra F L], (∀ (x : E), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits) → Fintype.card (E →ₐ[F] L) = Module.finrank F E
- Defined in
- Mathlib.FieldTheory.PrimitiveElement
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 159 from the axioms · uses propext, Classical.choice, Quot.sound
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.algebraMapstatement and proof · cited by 4,706
- AlgHomstatement · cited by 3,236
- FiniteDimensionalstatement and proof · cited by 1,854
- Module.finrankstatement and proof · cited by 1,770
- Fintype.cardstatement · cited by 1,386
- Polynomial.mapstatement and proof · cited by 806
- minpolystatement and proof · cited by 439
- Polynomial.Splitsstatement and proof · cited by 290
- Algebra.IsSeparablestatement and proof · cited by 210
- Fintype.card_eq_nat_cardproof · cited by 31
Cited by3
Results whose statement or proof uses this declaration.
- AlgHom.cardproof · cited by 10
- Field.primitive_element_iff_algHom_eq_of_eval'proof · cited by 1
- Field.primitive_element_iff_algHom_eq_of_evalproof · cited by 1