Theorem: KummersLemma.isUnramified (FltRegular/NumberTheory/KummersLemma/Field.lean)

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
L : Type u_2
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
⊢ IsUnramified (𝓞 K) (𝓞 L)
Tactic:
let α := polyRoot hp hζ u hcong _ (rootOfSplitsXPowSubC_pow p.pos _ L) 0
State after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
L : Type u_2
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
α : 𝓞 L := polyRoot hp hζ u hcong (rootOfSplitsXPowSubC ⋯ ((algebraMap (𝓞 K) K) ↑u) L) ⋯ 0
⊢ IsUnramified (𝓞 K) (𝓞 L)

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
L : Type u_2
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
α : 𝓞 L := polyRoot hp hζ u hcong (rootOfSplitsXPowSubC ⋯ ((algebraMap (𝓞 K) K) ↑u) L) ⋯ 0
⊢ IsUnramified (𝓞 K) (𝓞 L)
Tactic:
haveI := Polynomial.IsSplittingField.finiteDimensional L (X ^ (p : ℕ) - C (u : K))
State after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
L : Type u_2
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
α : 𝓞 L := polyRoot hp hζ u hcong (rootOfSplitsXPowSubC ⋯ ((algebraMap (𝓞 K) K) ↑u) L) ⋯ 0
this : FiniteDimensional K L
⊢ IsUnramified (𝓞 K) (𝓞 L)

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
L : Type u_2
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
α : 𝓞 L := polyRoot hp hζ u hcong (rootOfSplitsXPowSubC ⋯ ((algebraMap (𝓞 K) K) ↑u) L) ⋯ 0
this : FiniteDimensional K L
⊢ IsUnramified (𝓞 K) (𝓞 L)
Tactic:
have hα : Algebra.adjoin K {(α : L)} = ⊤ := by
  rw [eq_top_iff, ← Algebra.adjoin_root_eq_top_of_isSplittingField
    ⟨ζ, (mem_primitiveRoots p.pos).mpr hζ⟩ (X_pow_sub_C_irreducible_of_prime hpri.out hu)
    (rootOfSplitsXPowSubC_pow p.pos (u : K) L), Algebra.adjoin_le_iff, Set.singleton_subset_iff]
  exact mem_adjoin_polyRoot hp hζ u hcong _ _ 0
State after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
L : Type u_2
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
α : 𝓞 L := polyRoot hp hζ u hcong (rootOfSplitsXPowSubC ⋯ ((algebraMap (𝓞 K) K) ↑u) L) ⋯ 0
this : FiniteDimensional K L
hα : Algebra.adjoin K {↑α} = ⊤
⊢ IsUnramified (𝓞 K) (𝓞 L)

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
L : Type u_2
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
α : 𝓞 L := polyRoot hp hζ u hcong (rootOfSplitsXPowSubC ⋯ ((algebraMap (𝓞 K) K) ↑u) L) ⋯ 0
this : FiniteDimensional K L
hα : Algebra.adjoin K {↑α} = ⊤
⊢ IsUnramified (𝓞 K) (𝓞 L)
Tactic:
constructor
State after:
case isUnramifiedAt
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
L : Type u_2
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
α : 𝓞 L := polyRoot hp hζ u hcong (rootOfSplitsXPowSubC ⋯ ((algebraMap (𝓞 K) K) ↑u) L) ⋯ 0
this : FiniteDimensional K L
hα : Algebra.adjoin K {↑α} = ⊤
⊢ ∀ (p : Ideal (𝓞 K)) [inst : p.IsPrime], p ≠ ⊥ → IsUnramifiedAt (𝓞 L) p

State before:
case isUnramifiedAt
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
L : Type u_2
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
α : 𝓞 L := polyRoot hp hζ u hcong (rootOfSplitsXPowSubC ⋯ ((algebraMap (𝓞 K) K) ↑u) L) ⋯ 0
this : FiniteDimensional K L
hα : Algebra.adjoin K {↑α} = ⊤
⊢ ∀ (p : Ideal (𝓞 K)) [inst : p.IsPrime], p ≠ ⊥ → IsUnramifiedAt (𝓞 L) p
Tactic:
intros I hI hIbot
State after:
case isUnramifiedAt
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
L : Type u_2
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
α : 𝓞 L := polyRoot hp hζ u hcong (rootOfSplitsXPowSubC ⋯ ((algebraMap (𝓞 K) K) ↑u) L) ⋯ 0
this : FiniteDimensional K L
hα : Algebra.adjoin K {↑α} = ⊤
I : Ideal (𝓞 K)
hI : I.IsPrime
hIbot : I ≠ ⊥
⊢ IsUnramifiedAt (𝓞 L) I

State before:
case isUnramifiedAt
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
L : Type u_2
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
α : 𝓞 L := polyRoot hp hζ u hcong (rootOfSplitsXPowSubC ⋯ ((algebraMap (𝓞 K) K) ↑u) L) ⋯ 0
this : FiniteDimensional K L
hα : Algebra.adjoin K {↑α} = ⊤
I : Ideal (𝓞 K)
hI : I.IsPrime
hIbot : I ≠ ⊥
⊢ IsUnramifiedAt (𝓞 L) I
Tactic:
refine isUnramifiedAt_of_Separable_minpoly (R := 𝓞 K) K (S := 𝓞 L) L I hIbot α ?_ hα ?_
State after:
case isUnramifiedAt.refine_1
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
L : Type u_2
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
α : 𝓞 L := polyRoot hp hζ u hcong (rootOfSplitsXPowSubC ⋯ ((algebraMap (𝓞 K) K) ↑u) L) ⋯ 0
this : FiniteDimensional K L
hα : Algebra.adjoin K {↑α} = ⊤
I : Ideal (𝓞 K)
hI : I.IsPrime
hIbot : I ≠ ⊥
⊢ IsIntegral (𝓞 K) ↑α

case isUnramifiedAt.refine_2
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
L : Type u_2
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
α : 𝓞 L := polyRoot hp hζ u hcong (rootOfSplitsXPowSubC ⋯ ((algebraMap (𝓞 K) K) ↑u) L) ⋯ 0
this : FiniteDimensional K L
hα : Algebra.adjoin K {↑α} = ⊤
I : Ideal (𝓞 K)
hI : I.IsPrime
hIbot : I ≠ ⊥
⊢ (map (Ideal.Quotient.mk I) (minpoly (𝓞 K) ↑α)).Separable

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
L : Type u_2
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
α : 𝓞 L := polyRoot hp hζ u hcong (rootOfSplitsXPowSubC ⋯ ((algebraMap (𝓞 K) K) ↑u) L) ⋯ 0
this : FiniteDimensional K L
⊢ Algebra.adjoin K {↑α} = ⊤
Tactic:
rw [eq_top_iff, ← Algebra.adjoin_root_eq_top_of_isSplittingField
  ⟨ζ, (mem_primitiveRoots p.pos).mpr hζ⟩ (X_pow_sub_C_irreducible_of_prime hpri.out hu)
  (rootOfSplitsXPowSubC_pow p.pos (u : K) L), Algebra.adjoin_le_iff, Set.singleton_subset_iff]
State after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
L : Type u_2
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
α : 𝓞 L := polyRoot hp hζ u hcong (rootOfSplitsXPowSubC ⋯ ((algebraMap (𝓞 K) K) ↑u) L) ⋯ 0
this : FiniteDimensional K L
⊢ rootOfSplitsXPowSubC ⋯ ((algebraMap (𝓞 K) K) ↑u) L ∈ ↑(Algebra.adjoin K {↑α})

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
L : Type u_2
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
α : 𝓞 L := polyRoot hp hζ u hcong (rootOfSplitsXPowSubC ⋯ ((algebraMap (𝓞 K) K) ↑u) L) ⋯ 0
this : FiniteDimensional K L
⊢ rootOfSplitsXPowSubC ⋯ ((algebraMap (𝓞 K) K) ↑u) L ∈ ↑(Algebra.adjoin K {↑α})
Tactic:
exact mem_adjoin_polyRoot hp hζ u hcong _ _ 0
State after:
no goals

State before:
case isUnramifiedAt.refine_1
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
L : Type u_2
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
α : 𝓞 L := polyRoot hp hζ u hcong (rootOfSplitsXPowSubC ⋯ ((algebraMap (𝓞 K) K) ↑u) L) ⋯ 0
this : FiniteDimensional K L
hα : Algebra.adjoin K {↑α} = ⊤
I : Ideal (𝓞 K)
hI : I.IsPrime
hIbot : I ≠ ⊥
⊢ IsIntegral (𝓞 K) ↑α
Tactic:
exact IsIntegral.tower_top α.prop
State after:
no goals

State before:
case isUnramifiedAt.refine_2
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
L : Type u_2
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
α : 𝓞 L := polyRoot hp hζ u hcong (rootOfSplitsXPowSubC ⋯ ((algebraMap (𝓞 K) K) ↑u) L) ⋯ 0
this : FiniteDimensional K L
hα : Algebra.adjoin K {↑α} = ⊤
I : Ideal (𝓞 K)
hI : I.IsPrime
hIbot : I ≠ ⊥
⊢ (map (Ideal.Quotient.mk I) (minpoly (𝓞 K) ↑α)).Separable
Tactic:
rw [minpoly_polyRoot' hp hζ u hcong hu]
State after:
case isUnramifiedAt.refine_2
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
L : Type u_2
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
α : 𝓞 L := polyRoot hp hζ u hcong (rootOfSplitsXPowSubC ⋯ ((algebraMap (𝓞 K) K) ↑u) L) ⋯ 0
this : FiniteDimensional K L
hα : Algebra.adjoin K {↑α} = ⊤
I : Ideal (𝓞 K)
hI : I.IsPrime
hIbot : I ≠ ⊥
⊢ (map (Ideal.Quotient.mk I) (poly hp hζ u hcong)).Separable

State before:
case isUnramifiedAt.refine_2
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
L : Type u_2
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
α : 𝓞 L := polyRoot hp hζ u hcong (rootOfSplitsXPowSubC ⋯ ((algebraMap (𝓞 K) K) ↑u) L) ⋯ 0
this : FiniteDimensional K L
hα : Algebra.adjoin K {↑α} = ⊤
I : Ideal (𝓞 K)
hI : I.IsPrime
hIbot : I ≠ ⊥
⊢ (map (Ideal.Quotient.mk I) (poly hp hζ u hcong)).Separable
Tactic:
haveI := hI.isMaximal hIbot
State after:
case isUnramifiedAt.refine_2
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
L : Type u_2
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
α : 𝓞 L := polyRoot hp hζ u hcong (rootOfSplitsXPowSubC ⋯ ((algebraMap (𝓞 K) K) ↑u) L) ⋯ 0
this✝ : FiniteDimensional K L
hα : Algebra.adjoin K {↑α} = ⊤
I : Ideal (𝓞 K)
hI : I.IsPrime
hIbot : I ≠ ⊥
this : I.IsMaximal
⊢ (map (Ideal.Quotient.mk I) (poly hp hζ u hcong)).Separable

State before:
case isUnramifiedAt.refine_2
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
L : Type u_2
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
α : 𝓞 L := polyRoot hp hζ u hcong (rootOfSplitsXPowSubC ⋯ ((algebraMap (𝓞 K) K) ↑u) L) ⋯ 0
this✝ : FiniteDimensional K L
hα : Algebra.adjoin K {↑α} = ⊤
I : Ideal (𝓞 K)
hI : I.IsPrime
hIbot : I ≠ ⊥
this : I.IsMaximal
⊢ (map (Ideal.Quotient.mk I) (poly hp hζ u hcong)).Separable
Tactic:
exact separable_poly hp hζ u hcong hu I
State after:
no goals