internlm/Lean-Github huggingface dataset:
Theorem: KummersLemma.separable_poly_aux
Proof state before:
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 * ⟨α, ⋯⟩)
Tactic:
simp only [polyRoot, map_sub, map_one, sub_div, one_div, map_sub,
  sub_sub_sub_cancel_left, map_mul, NumberField.RingOfIntegers.map_mk]
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 ⟨α, ⋯⟩
⊢ ζ ^ j • α / ((algebraMap K L) ζ - 1) - ζ ^ i • α / ((algebraMap K L) ζ - 1) =
    (algebraMap (𝓞 L) L) ((algebraMap (𝓞 K) (𝓞 L)) ↑v) * α
Theorem: KummersLemma.separable_poly_aux
Proof state before:
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 ⟨α, ⋯⟩
⊢ ζ ^ j • α / ((algebraMap K L) ζ - 1) - ζ ^ i • α / ((algebraMap K L) ζ - 1) =
    (algebraMap (𝓞 L) L) ((algebraMap (𝓞 K) (𝓞 L)) ↑v) * α
Tactic:
rw [← sub_div, ← sub_smul, ← hv, Algebra.smul_def, map_mul, map_sub, map_one, mul_assoc,
  mul_div_cancel_left₀ _ hζ']
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 ⟨α, ⋯⟩
⊢ (algebraMap K L) ((algebraMap (𝓞 K) K) ↑v) * α = (algebraMap (𝓞 L) L) ((algebraMap (𝓞 K) (𝓞 L)) ↑v) * α
Theorem: KummersLemma.separable_poly_aux
Proof state before:
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 ⟨α, ⋯⟩
⊢ (algebraMap K L) ((algebraMap (𝓞 K) K) ↑v) * α = (algebraMap (𝓞 L) L) ((algebraMap (𝓞 K) (𝓞 L)) ↑v) * α
Tactic:
rfl
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)
⊢ (algebraMap K L) ζ - 1 ≠ 0
Tactic:
simpa using (algebraMap K L).injective.ne (hζ.sub_one_ne_zero hpri.out.one_lt)
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)
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)
Tactic:
refine hζ.unit'_coe.associated_sub_one hpri.out ?_ ?_ ?_
Proof state after:
case 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
α : 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
⊢ ↑hζ.unit' ^ j ∈ nthRootsFinset (↑p) (𝓞 K)

case 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
α : 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
⊢ ↑hζ.unit' ^ i ∈ nthRootsFinset (↑p) (𝓞 K)

case refine_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
⊢ ↑hζ.unit' ^ j ≠ ↑hζ.unit' ^ i
Theorem: KummersLemma.separable_poly_aux
Proof state before:
case 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
α : 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
⊢ ↑hζ.unit' ^ j ∈ nthRootsFinset (↑p) (𝓞 K)
Tactic:
rw [mem_nthRootsFinset p.pos, ← pow_mul, mul_comm, pow_mul, hζ.unit'_coe.pow_eq_one, one_pow]
Proof state after:
no goals
Theorem: KummersLemma.separable_poly_aux
Proof state before:
case 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
α : 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
⊢ ↑hζ.unit' ^ i ∈ nthRootsFinset (↑p) (𝓞 K)
Tactic:
rw [mem_nthRootsFinset p.pos, ← pow_mul, mul_comm, pow_mul, hζ.unit'_coe.pow_eq_one, one_pow]
Proof state after:
no goals
Theorem: KummersLemma.separable_poly_aux
Proof state before:
case refine_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
⊢ ↑hζ.unit' ^ j ≠ ↑hζ.unit' ^ i
Tactic:
exact mt (hζ.unit'_coe.injOn_pow hj hi) hij.symm
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)
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
⊢ IsIntegral (𝓞 K) α
Tactic:
apply IsIntegral.of_pow p.pos
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
v : (𝓞 K)ˣ
hcoe : (algebraMap (𝓞 K) K) ↑hζ.unit' = ζ
hv : (ζ - 1) * (algebraMap (𝓞 K) K) ↑v = ζ ^ j - ζ ^ i
⊢ IsIntegral (𝓞 K) (α ^ ↑p)
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
v : (𝓞 K)ˣ
hcoe : (algebraMap (𝓞 K) K) ↑hζ.unit' = ζ
hv : (ζ - 1) * (algebraMap (𝓞 K) K) ↑v = ζ ^ j - ζ ^ i
⊢ IsIntegral (𝓞 K) (α ^ ↑p)
Tactic:
rw [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 : ℕ
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
⊢ IsIntegral (𝓞 K) ((algebraMap K L) ((algebraMap (𝓞 K) K) ↑u))
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
v : (𝓞 K)ˣ
hcoe : (algebraMap (𝓞 K) K) ↑hζ.unit' = ζ
hv : (ζ - 1) * (algebraMap (𝓞 K) K) ↑v = ζ ^ j - ζ ^ i
⊢ IsIntegral (𝓞 K) ((algebraMap K L) ((algebraMap (𝓞 K) K) ↑u))
Tactic:
exact isIntegral_algebraMap
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)
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 ⟨α, ⋯⟩
Tactic:
rw [← isUnit_pow_iff p.pos.ne.symm]
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
v : (𝓞 K)ˣ
hcoe : (algebraMap (𝓞 K) K) ↑hζ.unit' = ζ
hv : (ζ - 1) * (algebraMap (𝓞 K) K) ↑v = ζ ^ j - ζ ^ i
hα : IsIntegral (𝓞 K) α
⊢ IsUnit (⟨α, ⋯⟩ ^ ↑p)
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
v : (𝓞 K)ˣ
hcoe : (algebraMap (𝓞 K) K) ↑hζ.unit' = ζ
hv : (ζ - 1) * (algebraMap (𝓞 K) K) ↑v = ζ ^ j - ζ ^ i
hα : IsIntegral (𝓞 K) α
⊢ IsUnit (⟨α, ⋯⟩ ^ ↑p)
Tactic:
convert (algebraMap (𝓞 K) (𝓞 L)).isUnit_map u.isUnit
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) α
e_1✝ : ↥(integralClosure ℤ L) = 𝓞 L
⊢ ⟨α, ⋯⟩ ^ ↑p = (algebraMap (𝓞 K) (𝓞 L)) ↑u
Theorem: KummersLemma.separable_poly_aux
Proof state before:
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) α
e_1✝ : ↥(integralClosure ℤ L) = 𝓞 L
⊢ ⟨α, ⋯⟩ ^ ↑p = (algebraMap (𝓞 K) (𝓞 L)) ↑u
Tactic:
ext
Proof state after:
case h.e'_3.h.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)
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) α
e_1✝ : ↥(integralClosure ℤ L) = 𝓞 L
⊢ ↑(⟨α, ⋯⟩ ^ ↑p) = ↑((algebraMap (𝓞 K) (𝓞 L)) ↑u)
Theorem: KummersLemma.separable_poly_aux
Proof state before:
case h.e'_3.h.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)
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) α
e_1✝ : ↥(integralClosure ℤ L) = 𝓞 L
⊢ ↑(⟨α, ⋯⟩ ^ ↑p) = ↑((algebraMap (𝓞 K) (𝓞 L)) ↑u)
Tactic:
simp only [SubmonoidClass.coe_pow, e]
Proof state after:
case h.e'_3.h.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)
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) α
e_1✝ : ↥(integralClosure ℤ L) = 𝓞 L
⊢ (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u) = ↑((algebraMap (𝓞 K) (𝓞 L)) ↑u)
Theorem: KummersLemma.separable_poly_aux
Proof state before:
case h.e'_3.h.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)
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) α
e_1✝ : ↥(integralClosure ℤ L) = 𝓞 L
⊢ (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u) = ↑((algebraMap (𝓞 K) (𝓞 L)) ↑u)
Tactic:
rfl
Proof state after:
no goals
Theorem: KummersLemma.separable_poly
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
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
⊢ (map (Ideal.Quotient.mk I) (poly hp hζ u hcong)).Separable
Tactic:
let L := K[(p : ℕ)√(u : K)]
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
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
L : Type u_1 := K[↑p√(algebraMap (𝓞 K) K) ↑u]
⊢ (map (Ideal.Quotient.mk I) (poly hp hζ u hcong)).Separable
Theorem: KummersLemma.separable_poly
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
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
L : Type u_1 := K[↑p√(algebraMap (𝓞 K) K) ↑u]
⊢ (map (Ideal.Quotient.mk I) (poly hp hζ u hcong)).Separable
Tactic:
letI := Fact.mk (X_pow_sub_C_irreducible_of_prime hpri.out hu)
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
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
L : Type u_1 := K[↑p√(algebraMap (𝓞 K) K) ↑u]
this : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
⊢ (map (Ideal.Quotient.mk I) (poly hp hζ u hcong)).Separable
Theorem: KummersLemma.separable_poly
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
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
L : Type u_1 := K[↑p√(algebraMap (𝓞 K) K) ↑u]
this : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
⊢ (map (Ideal.Quotient.mk I) (poly hp hζ u hcong)).Separable
Tactic:
let J := I.map (algebraMap (𝓞 K) (𝓞 L))
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
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
L : Type u_1 := K[↑p√(algebraMap (𝓞 K) K) ↑u]
this : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
J : Ideal (𝓞 L) := Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I
⊢ (map (Ideal.Quotient.mk I) (poly hp hζ u hcong)).Separable
Theorem: KummersLemma.separable_poly
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
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
L : Type u_1 := K[↑p√(algebraMap (𝓞 K) K) ↑u]
this : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
J : Ideal (𝓞 L) := Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I
⊢ (map (Ideal.Quotient.mk I) (poly hp hζ u hcong)).Separable
Tactic:
letI : AddCommGroup (𝓞 L) := AddCommGroupWithOne.toAddCommGroup
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
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
L : Type u_1 := K[↑p√(algebraMap (𝓞 K) K) ↑u]
this✝ : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
J : Ideal (𝓞 L) := Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I
this : AddCommGroup (𝓞 L) := AddCommGroupWithOne.toAddCommGroup
⊢ (map (Ideal.Quotient.mk I) (poly hp hζ u hcong)).Separable