Theorems · Theorem · number theory
FiniteField.nonempty_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], Module.finrank F K ∣ Module.finrank F L → Nonempty (K →ₐ[F] L)- Defined in
- Mathlib.FieldTheory.Finite.GaloisField
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 144 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites27
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Algebrastatement and proof · cited by 11,388
- Fintypeproof · cited by 7,736
- Fieldstatement and proof · cited by 7,404
- Algebra.algebraMapproof · cited by 4,706
- AlgHomstatement · cited by 3,236
- Finitestatement and proof · cited by 3,029
- Module.finrankstatement and proof · cited by 1,770
- Polynomial.Xproof · cited by 1,639
- Fintype.cardproof · cited by 1,386
- Module.Finiteproof · cited by 1,032
- Polynomial.mapproof · cited by 806
Cited by3
Results whose statement or proof uses this declaration.
- FiniteField.natCard_algHom_of_finrank_dvdproof · cited by 1
- FiniteField.nonempty_algHom_extensionproof · cited by 0
- FiniteField.nonempty_algHom_iff_finrank_dvdproof · cited by 0