Theorems · Theorem · field theory
normal_iff
∀ {F : Type u_1} {K : Type u_2} [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra F K],
Normal F K ↔ ∀ (x : K), IsIntegral F x ∧ (Polynomial.map (algebraMap F K) (minpoly F x)).Splits- Defined in
- Mathlib.FieldTheory.Normal.Defs
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 119 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
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
- Polynomial.mapstatement and proof · cited by 806
- minpolystatement and proof · cited by 439
- IsIntegralstatement and proof · cited by 427
- Polynomial.Splitsstatement and proof · cited by 290
- Normalstatement and proof · cited by 92
- Normal.splitsproof · cited by 7
- Normal.isIntegralproof · cited by 6
Cited by7
Results whose statement or proof uses this declaration.
- Normal.of_algEquivproof · cited by 4
- IsConjRoot.exists_algEquivproof · cited by 1
- Normal.of_equiv_equivproof · cited by 1
- Normal.outproof · cited by 1
- Normal.minpoly_eq_iff_mem_orbitproof · cited by 1
- Normal.of_isSplittingFieldproof · cited by 0
- Normal.tower_top_of_normalproof · cited by 0