Theorems · Theorem · field theory
Polynomial.separable_map
∀ {F : Type u} [inst : Field F] {S : Type u_1} [inst_1 : CommRing S] [Nontrivial S] (f : F →+* S) {p : Polynomial F},
(Polynomial.map f p).Separable ↔ p.Separable- Defined in
- Mathlib.FieldTheory.Separable
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 125 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- FieldCommRingNontrivial
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites19
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommRingstatement and proof · cited by 17,173
- RingHomstatement and proof · cited by 10,189
- Fieldstatement and proof · cited by 7,404
- Polynomialstatement and proof · cited by 5,681
- Idealproof · cited by 4,748
- Nontrivialstatement and proof · cited by 2,416
- HasQuotient.Quotientproof · cited by 2,301
- RingHom.compproof · cited by 899
- Polynomial.mapstatement and proof · cited by 806
- Ideal.Quotient.mkproof · cited by 610
- Ideal.IsMaximalproof · cited by 452
- IsCoprimeproof · cited by 321
Cited by6
Results whose statement or proof uses this declaration.
- AlgHom.natCard_of_powerBasisproof · cited by 2
- Polynomial.nodup_aroots_iff_of_splitsproof · cited by 1
- Polynomial.Gal.galActionHom_bijective_of_prime_degreeproof · cited by 1
- trace_eq_sum_embeddings_genproof · cited by 1
- Polynomial.separable_X_pow_sub_C_of_irreducibleproof · cited by 1
- IsGalois.of_separable_splitting_field_auxproof · cited by 0