internlm/Lean-Github huggingface dataset:
Theorem: KummersLemma.minpoly_polyRoot
Proof 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
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
i : ℕ
⊢ minpoly (𝓞 K) (polyRoot hp hζ u hcong α e i) = poly hp hζ u hcong
Tactic:
apply map_injective (algebraMap (𝓞 K) K) Subtype.coe_injective
Proof state after:
case a
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
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
i : ℕ
⊢ map (algebraMap (𝓞 K) K) (minpoly (𝓞 K) (polyRoot hp hζ u hcong α e i)) =
    map (algebraMap (𝓞 K) K) (poly hp hζ u hcong)
Theorem: KummersLemma.minpoly_polyRoot
Proof state before:
case a
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
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
i : ℕ
⊢ map (algebraMap (𝓞 K) K) (minpoly (𝓞 K) (polyRoot hp hζ u hcong α e i)) =
    map (algebraMap (𝓞 K) K) (poly hp hζ u hcong)
Tactic:
rw [← minpoly.isIntegrallyClosed_eq_field_fractions K L]
Proof state after:
case a
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
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
i : ℕ
⊢ minpoly K ((algebraMap (𝓞 L) L) (polyRoot hp hζ u hcong α e i)) = map (algebraMap (𝓞 K) K) (poly hp hζ u hcong)

case a
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
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
i : ℕ
⊢ IsIntegral (𝓞 K) (polyRoot hp hζ u hcong α e i)
Theorem: KummersLemma.minpoly_polyRoot
Proof state before:
case a
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
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
i : ℕ
⊢ minpoly K ((algebraMap (𝓞 L) L) (polyRoot hp hζ u hcong α e i)) = map (algebraMap (𝓞 K) K) (poly hp hζ u hcong)

case a
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
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
i : ℕ
⊢ IsIntegral (𝓞 K) (polyRoot hp hζ u hcong α e i)
Tactic:
exact minpoly_polyRoot'' hp hζ u hcong hu α e i
Proof state after:
case a
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
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
i : ℕ
⊢ IsIntegral (𝓞 K) (polyRoot hp hζ u hcong α e i)
Theorem: KummersLemma.minpoly_polyRoot
Proof state before:
case a
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
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
i : ℕ
⊢ IsIntegral (𝓞 K) (polyRoot hp hζ u hcong α e i)
Tactic:
exact IsIntegralClosure.isIntegral _ L (polyRoot hp hζ u hcong α e i)
Proof state after:
no goals
Theorem: KummersLemma.separable_poly_aux
Proof 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
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
⊢ (map (algebraMap (𝓞 K) (𝓞 L)) (poly hp hζ u hcong)).Separable
Tactic:
have hζ' : algebraMap K L ζ - 1 ≠ 0 := by
  simpa using (algebraMap K L).injective.ne (hζ.sub_one_ne_zero hpri.out.one_lt)
Proof 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
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
hζ' : (algebraMap K L) ζ - 1 ≠ 0
⊢ (map (algebraMap (𝓞 K) (𝓞 L)) (poly hp hζ u hcong)).Separable
Theorem: KummersLemma.separable_poly_aux
Proof 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
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
hζ' : (algebraMap K L) ζ - 1 ≠ 0
⊢ (map (algebraMap (𝓞 K) (𝓞 L)) (poly hp hζ u hcong)).Separable
Tactic:
rw [map_poly_eq_prod (e := e)]
Proof 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
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
hζ' : (algebraMap K L) ζ - 1 ≠ 0
⊢ (∏ i ∈ Finset.range ↑p, (X - C (polyRoot hp hζ u hcong α e i))).Separable
Theorem: KummersLemma.separable_poly_aux
Proof 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
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
hζ' : (algebraMap K L) ζ - 1 ≠ 0
⊢ (∏ i ∈ Finset.range ↑p, (X - C (polyRoot hp hζ u hcong α e i))).Separable
Tactic:
refine separable_prod' ?_ (fun _ _ => separable_X_sub_C)
Proof 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
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
hζ' : (algebraMap K L) ζ - 1 ≠ 0
⊢ ∀ x ∈ Finset.range ↑p,
    ∀ y ∈ Finset.range ↑p,
      x ≠ y → IsCoprime (X - C (polyRoot hp hζ u hcong α e x)) (X - C (polyRoot hp hζ u hcong α e y))
Theorem: KummersLemma.separable_poly_aux
Proof 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
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
hζ' : (algebraMap K L) ζ - 1 ≠ 0
⊢ ∀ x ∈ Finset.range ↑p,
    ∀ y ∈ Finset.range ↑p,
      x ≠ y → IsCoprime (X - C (polyRoot hp hζ u hcong α e x)) (X - C (polyRoot hp hζ u hcong α e y))
Tactic:
intros i hi j hj hij
Proof 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
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
hζ' : (algebraMap K L) ζ - 1 ≠ 0
i : ℕ
hi : i ∈ Finset.range ↑p
j : ℕ
hj : j ∈ Finset.range ↑p
hij : i ≠ j
⊢ IsCoprime (X - C (polyRoot hp hζ u hcong α e i)) (X - C (polyRoot hp hζ u hcong α e j))
Theorem: KummersLemma.separable_poly_aux
Proof 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
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
hζ' : (algebraMap K L) ζ - 1 ≠ 0
i : ℕ
hi : i ∈ Finset.range ↑p
j : ℕ
hj : j ∈ Finset.range ↑p
hij : i ≠ j
⊢ IsCoprime (X - C (polyRoot hp hζ u hcong α e i)) (X - C (polyRoot hp hζ u hcong α e j))
Tactic:
apply isCoprime_X_sub_C_of_isUnit_sub
Proof state after:
case h
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
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
hζ' : (algebraMap K L) ζ - 1 ≠ 0
i : ℕ
hi : i ∈ Finset.range ↑p
j : ℕ
hj : j ∈ Finset.range ↑p
hij : i ≠ j
⊢ IsUnit (polyRoot hp hζ u hcong α e i - polyRoot hp hζ u hcong α e j)
Theorem: KummersLemma.separable_poly_aux
Proof state before:
case h
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
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
hζ' : (algebraMap K L) ζ - 1 ≠ 0
i : ℕ
hi : i ∈ Finset.range ↑p
j : ℕ
hj : j ∈ Finset.range ↑p
hij : i ≠ j
⊢ IsUnit (polyRoot hp hζ u hcong α e i - polyRoot hp hζ u hcong α e j)
Tactic:
obtain ⟨v, hv⟩ : Associated (hζ.unit' - 1 : 𝓞 K) ((hζ.unit' : 𝓞 K) ^ j - (hζ.unit' : 𝓞 K) ^ i)
Proof 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
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
hζ' : (algebraMap K L) ζ - 1 ≠ 0
i : ℕ
hi : i ∈ Finset.range ↑p
j : ℕ
hj : j ∈ Finset.range ↑p
hij : i ≠ j
⊢ Associated (↑hζ.unit' - 1) (↑hζ.unit' ^ j - ↑hζ.unit' ^ i)

case h.intro
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
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
hζ' : (algebraMap K L) ζ - 1 ≠ 0
i : ℕ
hi : i ∈ Finset.range ↑p
j : ℕ
hj : j ∈ Finset.range ↑p
hij : i ≠ j
v : (𝓞 K)ˣ
hv : (↑hζ.unit' - 1) * ↑v = ↑hζ.unit' ^ j - ↑hζ.unit' ^ i
⊢ IsUnit (polyRoot hp hζ u hcong α e i - polyRoot hp hζ u hcong α e j)
Theorem: KummersLemma.separable_poly_aux
Proof state before:
case h.intro
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
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
hζ' : (algebraMap K L) ζ - 1 ≠ 0
i : ℕ
hi : i ∈ Finset.range ↑p
j : ℕ
hj : j ∈ Finset.range ↑p
hij : i ≠ j
v : (𝓞 K)ˣ
hv : (↑hζ.unit' - 1) * ↑v = ↑hζ.unit' ^ j - ↑hζ.unit' ^ i
⊢ IsUnit (polyRoot hp hζ u hcong α e i - polyRoot hp hζ u hcong α e j)
Tactic:
rw [NumberField.RingOfIntegers.ext_iff] at hv
Proof state after:
case h.intro
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
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
hζ' : (algebraMap K L) ζ - 1 ≠ 0
i : ℕ
hi : i ∈ Finset.range ↑p
j : ℕ
hj : j ∈ Finset.range ↑p
hij : i ≠ j
v : (𝓞 K)ˣ
hv : ↑((↑hζ.unit' - 1) * ↑v) = ↑(↑hζ.unit' ^ j - ↑hζ.unit' ^ i)
⊢ IsUnit (polyRoot hp hζ u hcong α e i - polyRoot hp hζ u hcong α e j)
Theorem: KummersLemma.separable_poly_aux
Proof state before:
case h.intro
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
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
hζ' : (algebraMap K L) ζ - 1 ≠ 0
i : ℕ
hi : i ∈ Finset.range ↑p
j : ℕ
hj : j ∈ Finset.range ↑p
hij : i ≠ j
v : (𝓞 K)ˣ
hv : ↑((↑hζ.unit' - 1) * ↑v) = ↑(↑hζ.unit' ^ j - ↑hζ.unit' ^ i)
⊢ IsUnit (polyRoot hp hζ u hcong α e i - polyRoot hp hζ u hcong α e j)
Tactic:
have hcoe : (algebraMap (𝓞 K) K) (↑hζ.unit') = ζ := rfl
Proof state after:
case h.intro
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
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
hζ' : (algebraMap K L) ζ - 1 ≠ 0
i : ℕ
hi : i ∈ Finset.range ↑p
j : ℕ
hj : j ∈ Finset.range ↑p
hij : i ≠ j
v : (𝓞 K)ˣ
hv : ↑((↑hζ.unit' - 1) * ↑v) = ↑(↑hζ.unit' ^ j - ↑hζ.unit' ^ i)
hcoe : (algebraMap (𝓞 K) K) ↑hζ.unit' = ζ
⊢ IsUnit (polyRoot hp hζ u hcong α e i - polyRoot hp hζ u hcong α e j)
Theorem: KummersLemma.separable_poly_aux
Proof state before:
case h.intro
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
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
hζ' : (algebraMap K L) ζ - 1 ≠ 0
i : ℕ
hi : i ∈ Finset.range ↑p
j : ℕ
hj : j ∈ Finset.range ↑p
hij : i ≠ j
v : (𝓞 K)ˣ
hv : ↑((↑hζ.unit' - 1) * ↑v) = ↑(↑hζ.unit' ^ j - ↑hζ.unit' ^ i)
hcoe : (algebraMap (𝓞 K) K) ↑hζ.unit' = ζ
⊢ IsUnit (polyRoot hp hζ u hcong α e i - polyRoot hp hζ u hcong α e j)
Tactic:
simp only [map_mul, map_sub, IsPrimitiveRoot.val_unit'_coe, map_one, map_pow, hcoe] at hv
Proof state after:
case h.intro
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
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
hζ' : (algebraMap K L) ζ - 1 ≠ 0
i : ℕ
hi : i ∈ Finset.range ↑p
j : ℕ
hj : j ∈ Finset.range ↑p
hij : i ≠ j
v : (𝓞 K)ˣ
hcoe : (algebraMap (𝓞 K) K) ↑hζ.unit' = ζ
hv : (ζ - 1) * (algebraMap (𝓞 K) K) ↑v = ζ ^ j - ζ ^ i
⊢ IsUnit (polyRoot hp hζ u hcong α e i - polyRoot hp hζ u hcong α e j)
Theorem: KummersLemma.separable_poly_aux
Proof state before:
case h.intro
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
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
hζ' : (algebraMap K L) ζ - 1 ≠ 0
i : ℕ
hi : i ∈ Finset.range ↑p
j : ℕ
hj : j ∈ Finset.range ↑p
hij : i ≠ j
v : (𝓞 K)ˣ
hcoe : (algebraMap (𝓞 K) K) ↑hζ.unit' = ζ
hv : (ζ - 1) * (algebraMap (𝓞 K) K) ↑v = ζ ^ j - ζ ^ i
⊢ IsUnit (polyRoot hp hζ u hcong α e i - polyRoot hp hζ u hcong α e j)
Tactic:
have hα : IsIntegral (𝓞 K) α := by
  apply IsIntegral.of_pow p.pos; rw [e]; exact isIntegral_algebraMap
Proof state after:
case h.intro
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
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
hζ' : (algebraMap K L) ζ - 1 ≠ 0
i : ℕ
hi : i ∈ Finset.range ↑p
j : ℕ
hj : j ∈ Finset.range ↑p
hij : i ≠ j
v : (𝓞 K)ˣ
hcoe : (algebraMap (𝓞 K) K) ↑hζ.unit' = ζ
hv : (ζ - 1) * (algebraMap (𝓞 K) K) ↑v = ζ ^ j - ζ ^ i
hα : IsIntegral (𝓞 K) α
⊢ IsUnit (polyRoot hp hζ u hcong α e i - polyRoot hp hζ u hcong α e j)
Theorem: KummersLemma.separable_poly_aux
Proof state before:
case h.intro
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
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
hζ' : (algebraMap K L) ζ - 1 ≠ 0
i : ℕ
hi : i ∈ Finset.range ↑p
j : ℕ
hj : j ∈ Finset.range ↑p
hij : i ≠ j
v : (𝓞 K)ˣ
hcoe : (algebraMap (𝓞 K) K) ↑hζ.unit' = ζ
hv : (ζ - 1) * (algebraMap (𝓞 K) K) ↑v = ζ ^ j - ζ ^ i
hα : IsIntegral (𝓞 K) α
⊢ IsUnit (polyRoot hp hζ u hcong α e i - polyRoot hp hζ u hcong α e j)
Tactic:
have : IsUnit (⟨α, isIntegral_trans _ hα⟩ : 𝓞 L) := by
  rw [← isUnit_pow_iff p.pos.ne.symm]
  convert (algebraMap (𝓞 K) (𝓞 L)).isUnit_map u.isUnit
  ext; simp only [SubmonoidClass.coe_pow, e]; rfl
Proof state after:
case h.intro
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
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
hζ' : (algebraMap K L) ζ - 1 ≠ 0
i : ℕ
hi : i ∈ Finset.range ↑p
j : ℕ
hj : j ∈ Finset.range ↑p
hij : i ≠ j
v : (𝓞 K)ˣ
hcoe : (algebraMap (𝓞 K) K) ↑hζ.unit' = ζ
hv : (ζ - 1) * (algebraMap (𝓞 K) K) ↑v = ζ ^ j - ζ ^ i
hα : IsIntegral (𝓞 K) α
this : IsUnit ⟨α, ⋯⟩
⊢ IsUnit (polyRoot hp hζ u hcong α e i - polyRoot hp hζ u hcong α e j)
Theorem: KummersLemma.separable_poly_aux
Proof state before:
case h.intro
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
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
hζ' : (algebraMap K L) ζ - 1 ≠ 0
i : ℕ
hi : i ∈ Finset.range ↑p
j : ℕ
hj : j ∈ Finset.range ↑p
hij : i ≠ j
v : (𝓞 K)ˣ
hcoe : (algebraMap (𝓞 K) K) ↑hζ.unit' = ζ
hv : (ζ - 1) * (algebraMap (𝓞 K) K) ↑v = ζ ^ j - ζ ^ i
hα : IsIntegral (𝓞 K) α
this : IsUnit ⟨α, ⋯⟩
⊢ IsUnit (polyRoot hp hζ u hcong α e i - polyRoot hp hζ u hcong α e j)
Tactic:
convert ((algebraMap (𝓞 K) (𝓞 L)).isUnit_map v.isUnit).mul this using 1
Proof state after:
case h.e'_3
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
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
hζ' : (algebraMap K L) ζ - 1 ≠ 0
i : ℕ
hi : i ∈ Finset.range ↑p
j : ℕ
hj : j ∈ Finset.range ↑p
hij : i ≠ j
v : (𝓞 K)ˣ
hcoe : (algebraMap (𝓞 K) K) ↑hζ.unit' = ζ
hv : (ζ - 1) * (algebraMap (𝓞 K) K) ↑v = ζ ^ j - ζ ^ i
hα : IsIntegral (𝓞 K) α
this : IsUnit ⟨α, ⋯⟩
⊢ polyRoot hp hζ u hcong α e i - polyRoot hp hζ u hcong α e j = (algebraMap (𝓞 K) (𝓞 L)) ↑v * ⟨α, ⋯⟩
Theorem: KummersLemma.separable_poly_aux
Proof state before:
case h.e'_3
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
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
hζ' : (algebraMap K L) ζ - 1 ≠ 0
i : ℕ
hi : i ∈ Finset.range ↑p
j : ℕ
hj : j ∈ Finset.range ↑p
hij : i ≠ j
v : (𝓞 K)ˣ
hcoe : (algebraMap (𝓞 K) K) ↑hζ.unit' = ζ
hv : (ζ - 1) * (algebraMap (𝓞 K) K) ↑v = ζ ^ j - ζ ^ i
hα : IsIntegral (𝓞 K) α
this : IsUnit ⟨α, ⋯⟩
⊢ polyRoot hp hζ u hcong α e i - polyRoot hp hζ u hcong α e j = (algebraMap (𝓞 K) (𝓞 L)) ↑v * ⟨α, ⋯⟩
Tactic:
ext
Proof state after:
case h.e'_3.h
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
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
hζ' : (algebraMap K L) ζ - 1 ≠ 0
i : ℕ
hi : i ∈ Finset.range ↑p
j : ℕ
hj : j ∈ Finset.range ↑p
hij : i ≠ j
v : (𝓞 K)ˣ
hcoe : (algebraMap (𝓞 K) K) ↑hζ.unit' = ζ
hv : (ζ - 1) * (algebraMap (𝓞 K) K) ↑v = ζ ^ j - ζ ^ i
hα : IsIntegral (𝓞 K) α
this : IsUnit ⟨α, ⋯⟩
⊢ ↑(polyRoot hp hζ u hcong α e i - polyRoot hp hζ u hcong α e j) = ↑((algebraMap (𝓞 K) (𝓞 L)) ↑v * ⟨α, ⋯⟩)