Theorems · Theorem · field theory
AlgHom.fieldRange_of_normal
∀ {F : Type u_1} {K : Type u_2} [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra F K] {E : IntermediateField F K}
[Normal F ↥E] (f : ↥E →ₐ[F] K), f.fieldRange = E- Defined in
- Mathlib.FieldTheory.Normal.Basic
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 148 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites18
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 and proof · cited by 3,236
- AlgEquivproof · cited by 1,681
- IntermediateFieldstatement and proof · cited by 988
- AlgHom.compproof · cited by 501
- AlgEquiv.toAlgHomproof · cited by 273
- DFunLike.ext_iffproof · cited by 102
- Normalstatement and proof · cited by 92
- IntermediateField.mapproof · cited by 62
- AlgHom.fieldRangestatement and proof · cited by 57
- IntermediateField.valproof · cited by 42
Cited by2
Results whose statement or proof uses this declaration.
- IntermediateField.normalClosure_of_normalproof · cited by 2
- IntermediateField.normal_iff_forall_fieldRange_eqproof · cited by 1