AlgebraicNumberTheory.Valuations.primitive_irreducible_reduction_natDegree_zero_of_leadingCoeff_nonunit_of_roots_eq
If the roots of a primitive irreducible polynomial all have the same value in a splitting field, then the nonunit-leading-coefficient branch has constant reduction.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open Polynomial
namespace AlgebraicNumberTheory
namespace Valuations
universe uLean source · statement
theorem primitive_irreducible_reduction_natDegree_zero_of_leadingCoeff_nonunit_of_roots_eq
{K L : Type u} [Field K] [Field L] [Algebra K L]
(V : ValuationSubring K) (B : ValuationSubring L)
[V.valuation.HasExtension B.valuation]
(Q : Polynomial V) (hQprim : Q.IsPrimitive)
(hQirr : Irreducible (Q.map V.subtype))
[IsSplittingField K L (Q.map V.subtype)]
(hlead : ¬ IsUnit Q.leadingCoeff)
(hrootsEq : ∀ {a b : L},
a ∈ ((Q.map V.subtype).map (algebraMap K L)).roots →
b ∈ ((Q.map V.subtype).map (algebraMap K L)).roots →
B.valuation a = B.valuation b) :
(Q.map (IsLocalRing.residue V)).natDegree = 0