Theorems · Theorem · field theory
Algebra.IsUnramifiedAt.not_minpoly_sq_dvd
∀ {K : Type u_1} {A : Type u_2} [inst : Field K] [inst_1 : CommRing A] [inst_2 : Algebra K A] (Q : Ideal A)
[inst_3 : Q.IsPrime] [Algebra.IsUnramifiedAt K Q] (x : A) (p : Polynomial K),
Ideal.span {p} = RingHom.ker (Polynomial.aeval x).toRingHom →
Function.Surjective ⇑(Polynomial.aeval x) → ¬minpoly K ((algebraMap A Q.ResidueField) x) ^ 2 ∣ pIf A = K[X]/⟨p⟩ is unramified at some prime Q, then the minpoly of X in κ(Q)
only divides p once.
- Defined in
- Mathlib.RingTheory.Unramified.Field
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 181 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites45
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Setstatement · cited by 53,352
- CommRingstatement and proof · cited by 17,173
- Algebrastatement and proof · cited by 11,388
- RingHomstatement · cited by 10,189
- Fieldstatement and proof · cited by 7,404
- Polynomialstatement and proof · cited by 5,681
- Idealstatement and proof · cited by 4,748
- Algebra.algebraMapstatement and proof · cited by 4,706
- AlgHomstatement · cited by 3,236
- map_zeroproof · cited by 1,614
- Module.Finiteproof · cited by 1,032
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.