theorem
DedekindCriterion.index_dvd_iff_span_eq_top
{K : Type u_1}
[Field K]
[NumberField K]
(α : NumberField.RingOfIntegers K)
(hK : ℚ[(algebraMap (NumberField.RingOfIntegers K) K) α] = ⊤)
(p : ℕ)
[hp : Fact (Nat.Prime p)]
(u v w : Polynomial ℤ)
(hu_monic : u.Monic)
(hv_monic : v.Monic)
(huv_bar :
Polynomial.map (Int.castRingHom (ZMod p)) u * Polynomial.map (Int.castRingHom (ZMod p)) v = Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ α))
(husq : Squarefree (Polynomial.map (Int.castRingHom (ZMod p)) u))
(hw : u * v - minpoly ℤ α = Polynomial.C ↑p * w)
:
p ∣ (Subalgebra.toSubmodule ℤ[α]).toAddSubgroup.index ↔ Ideal.span
{Polynomial.map (Int.castRingHom (ZMod p)) u, Polynomial.map (Int.castRingHom (ZMod p)) v, Polynomial.map (Int.castRingHom (ZMod p)) w} = ⊤
theorem
dedekind_criterion
{K : Type u_1}
[Field K]
[NumberField K]
(α : NumberField.RingOfIntegers K)
(hK : ℚ[(algebraMap (NumberField.RingOfIntegers K) K) α] = ⊤)
(p : ℕ)
[hp : Fact (Nat.Prime p)]
(u v w : Polynomial ℤ)
(hu_monic : u.Monic)
(hv_monic : v.Monic)
(huv_bar :
Polynomial.map (Int.castRingHom (ZMod p)) u * Polynomial.map (Int.castRingHom (ZMod p)) v = Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ α))
(husq : Squarefree (Polynomial.map (Int.castRingHom (ZMod p)) u))
(hw : u * v - minpoly ℤ α = Polynomial.C ↑p * w)
:
p ∣ (Subalgebra.toSubmodule ℤ[α]).toAddSubgroup.index ↔ Ideal.span
{Polynomial.map (Int.castRingHom (ZMod p)) u, Polynomial.map (Int.castRingHom (ZMod p)) v, Polynomial.map (Int.castRingHom (ZMod p)) w} = ⊤