internlm/Lean-Github huggingface dataset:
Theorem: KummersLemma.roots_poly
Proof state before:
case neg
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α : ¬α = 0
⊢ (map (algebraMap (𝓞 K) L) (poly hp hζ u hcong)).roots =
    Multiset.map (fun i => (1 - ζ ^ i • α) / (algebraMap K L) (ζ - 1)) (Finset.range ↑p).val
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:
case neg
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α : ¬α = 0
hζ' : (algebraMap K L) ζ - 1 ≠ 0
⊢ (map (algebraMap (𝓞 K) L) (poly hp hζ u hcong)).roots =
    Multiset.map (fun i => (1 - ζ ^ i • α) / (algebraMap K L) (ζ - 1)) (Finset.range ↑p).val
Theorem: KummersLemma.roots_poly
Proof state before:
case pos
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α : α = 0
⊢ (map (algebraMap (𝓞 K) L) (poly hp hζ u hcong)).roots =
    Multiset.map (fun i => (1 - ζ ^ i • α) / (algebraMap K L) (ζ - 1)) (Finset.range ↑p).val
Tactic:
rw [hα, zero_pow p.ne_zero] at e
Proof state after:
case pos
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 : 0 = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
hα : α = 0
⊢ (map (algebraMap (𝓞 K) L) (poly hp hζ u hcong)).roots =
    Multiset.map (fun i => (1 - ζ ^ i • α) / (algebraMap K L) (ζ - 1)) (Finset.range ↑p).val
Theorem: KummersLemma.roots_poly
Proof state before:
case pos
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 : 0 = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
hα : α = 0
⊢ (map (algebraMap (𝓞 K) L) (poly hp hζ u hcong)).roots =
    Multiset.map (fun i => (1 - ζ ^ i • α) / (algebraMap K L) (ζ - 1)) (Finset.range ↑p).val
Tactic:
exact (((algebraMap (𝓞 K) L).isUnit_map u.isUnit).ne_zero e.symm).elim
Proof state after:
no goals
Theorem: KummersLemma.roots_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
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
hα : ¬α = 0
⊢ (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.roots_poly
Proof state before:
case neg
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α : ¬α = 0
hζ' : (algebraMap K L) ζ - 1 ≠ 0
⊢ (map (algebraMap (𝓞 K) L) (poly hp hζ u hcong)).roots =
    Multiset.map (fun i => (1 - ζ ^ i • α) / (algebraMap K L) (ζ - 1)) (Finset.range ↑p).val
Tactic:
symm
Proof state after:
case neg
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α : ¬α = 0
hζ' : (algebraMap K L) ζ - 1 ≠ 0
⊢ Multiset.map (fun i => (1 - ζ ^ i • α) / (algebraMap K L) (ζ - 1)) (Finset.range ↑p).val =
    (map (algebraMap (𝓞 K) L) (poly hp hζ u hcong)).roots
Theorem: KummersLemma.roots_poly
Proof state before:
case neg
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α : ¬α = 0
hζ' : (algebraMap K L) ζ - 1 ≠ 0
⊢ Multiset.map (fun i => (1 - ζ ^ i • α) / (algebraMap K L) (ζ - 1)) (Finset.range ↑p).val =
    (map (algebraMap (𝓞 K) L) (poly hp hζ u hcong)).roots
Tactic:
apply Multiset.eq_of_le_of_card_le
Proof state after:
case neg.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α : ¬α = 0
hζ' : (algebraMap K L) ζ - 1 ≠ 0
⊢ Multiset.map (fun i => (1 - ζ ^ i • α) / (algebraMap K L) (ζ - 1)) (Finset.range ↑p).val ≤
    (map (algebraMap (𝓞 K) L) (poly hp hζ u hcong)).roots

case neg.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α : ¬α = 0
hζ' : (algebraMap K L) ζ - 1 ≠ 0
⊢ Multiset.card (map (algebraMap (𝓞 K) L) (poly hp hζ u hcong)).roots ≤
    Multiset.card (Multiset.map (fun i => (1 - ζ ^ i • α) / (algebraMap K L) (ζ - 1)) (Finset.range ↑p).val)
Theorem: KummersLemma.roots_poly
Proof state before:
case neg.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α : ¬α = 0
hζ' : (algebraMap K L) ζ - 1 ≠ 0
⊢ Multiset.map (fun i => (1 - ζ ^ i • α) / (algebraMap K L) (ζ - 1)) (Finset.range ↑p).val ≤
    (map (algebraMap (𝓞 K) L) (poly hp hζ u hcong)).roots
Tactic:
rw [← Finset.image_val_of_injOn, Finset.val_le_iff_val_subset]
Proof state after:
case neg.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α : ¬α = 0
hζ' : (algebraMap K L) ζ - 1 ≠ 0
⊢ (Finset.image (fun i => (1 - ζ ^ i • α) / (algebraMap K L) (ζ - 1)) (Finset.range ↑p)).val ⊆
    (map (algebraMap (𝓞 K) L) (poly hp hζ u hcong)).roots

case neg.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α : ¬α = 0
hζ' : (algebraMap K L) ζ - 1 ≠ 0
⊢ Set.InjOn (fun i => (1 - ζ ^ i • α) / (algebraMap K L) (ζ - 1)) ↑(Finset.range ↑p)
Theorem: KummersLemma.roots_poly
Proof state before:
case neg.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α : ¬α = 0
hζ' : (algebraMap K L) ζ - 1 ≠ 0
⊢ (Finset.image (fun i => (1 - ζ ^ i • α) / (algebraMap K L) (ζ - 1)) (Finset.range ↑p)).val ⊆
    (map (algebraMap (𝓞 K) L) (poly hp hζ u hcong)).roots
Tactic:
intro x hx
Proof state after:
case neg.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α : ¬α = 0
hζ' : (algebraMap K L) ζ - 1 ≠ 0
x : L
hx : x ∈ (Finset.image (fun i => (1 - ζ ^ i • α) / (algebraMap K L) (ζ - 1)) (Finset.range ↑p)).val
⊢ x ∈ (map (algebraMap (𝓞 K) L) (poly hp hζ u hcong)).roots
Theorem: KummersLemma.roots_poly
Proof state before:
case neg.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α : ¬α = 0
hζ' : (algebraMap K L) ζ - 1 ≠ 0
x : L
hx : x ∈ (Finset.image (fun i => (1 - ζ ^ i • α) / (algebraMap K L) (ζ - 1)) (Finset.range ↑p)).val
⊢ x ∈ (map (algebraMap (𝓞 K) L) (poly hp hζ u hcong)).roots
Tactic:
simp only [Finset.image_val, Finset.range_val, Multiset.mem_dedup, Multiset.mem_map,
  Multiset.mem_range] at hx
Proof state after:
case neg.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α : ¬α = 0
hζ' : (algebraMap K L) ζ - 1 ≠ 0
x : L
hx : ∃ a < ↑p, (1 - ζ ^ a • α) / (algebraMap K L) (ζ - 1) = x
⊢ x ∈ (map (algebraMap (𝓞 K) L) (poly hp hζ u hcong)).roots
Theorem: KummersLemma.roots_poly
Proof state before:
case neg.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α : ¬α = 0
hζ' : (algebraMap K L) ζ - 1 ≠ 0
x : L
hx : ∃ a < ↑p, (1 - ζ ^ a • α) / (algebraMap K L) (ζ - 1) = x
⊢ x ∈ (map (algebraMap (𝓞 K) L) (poly hp hζ u hcong)).roots
Tactic:
obtain ⟨m, _, rfl⟩ := hx
Proof state after:
case neg.h.intro.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α : ¬α = 0
hζ' : (algebraMap K L) ζ - 1 ≠ 0
m : ℕ
left✝ : m < ↑p
⊢ (1 - ζ ^ m • α) / (algebraMap K L) (ζ - 1) ∈ (map (algebraMap (𝓞 K) L) (poly hp hζ u hcong)).roots
Theorem: KummersLemma.roots_poly
Proof state before:
case neg.h.intro.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α : ¬α = 0
hζ' : (algebraMap K L) ζ - 1 ≠ 0
m : ℕ
left✝ : m < ↑p
⊢ (1 - ζ ^ m • α) / (algebraMap K L) (ζ - 1) ∈ (map (algebraMap (𝓞 K) L) (poly hp hζ u hcong)).roots
Tactic:
rw [mem_roots, IsRoot.def, eval_map, ← aeval_def, aeval_poly hp hζ u hcong α e]
Proof state after:
case neg.h.intro.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α : ¬α = 0
hζ' : (algebraMap K L) ζ - 1 ≠ 0
m : ℕ
left✝ : m < ↑p
⊢ map (algebraMap (𝓞 K) L) (poly hp hζ u hcong) ≠ 0
Theorem: KummersLemma.roots_poly
Proof state before:
case neg.h.intro.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α : ¬α = 0
hζ' : (algebraMap K L) ζ - 1 ≠ 0
m : ℕ
left✝ : m < ↑p
⊢ map (algebraMap (𝓞 K) L) (poly hp hζ u hcong) ≠ 0
Tactic:
exact ((monic_poly hp hζ u hcong).map (algebraMap (𝓞 K) L)).ne_zero
Proof state after:
no goals
Theorem: KummersLemma.roots_poly
Proof state before:
case neg.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α : ¬α = 0
hζ' : (algebraMap K L) ζ - 1 ≠ 0
⊢ Set.InjOn (fun i => (1 - ζ ^ i • α) / (algebraMap K L) (ζ - 1)) ↑(Finset.range ↑p)
Tactic:
intros i hi j hj e
Proof state after:
case neg.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α : ¬α = 0
hζ' : (algebraMap K L) ζ - 1 ≠ 0
i : ℕ
hi : i ∈ ↑(Finset.range ↑p)
j : ℕ
hj : j ∈ ↑(Finset.range ↑p)
e : (fun i => (1 - ζ ^ i • α) / (algebraMap K L) (ζ - 1)) i = (fun i => (1 - ζ ^ i • α) / (algebraMap K L) (ζ - 1)) j
⊢ i = j
Theorem: KummersLemma.roots_poly
Proof state before:
case neg.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α : ¬α = 0
hζ' : (algebraMap K L) ζ - 1 ≠ 0
i : ℕ
hi : i ∈ ↑(Finset.range ↑p)
j : ℕ
hj : j ∈ ↑(Finset.range ↑p)
e : (fun i => (1 - ζ ^ i • α) / (algebraMap K L) (ζ - 1)) i = (fun i => (1 - ζ ^ i • α) / (algebraMap K L) (ζ - 1)) j
⊢ i = j
Tactic:
apply (hζ.map_of_injective (algebraMap K L).injective).injOn_pow_mul hα hi hj
Proof state after:
case neg.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α : ¬α = 0
hζ' : (algebraMap K L) ζ - 1 ≠ 0
i : ℕ
hi : i ∈ ↑(Finset.range ↑p)
j : ℕ
hj : j ∈ ↑(Finset.range ↑p)
e : (fun i => (1 - ζ ^ i • α) / (algebraMap K L) (ζ - 1)) i = (fun i => (1 - ζ ^ i • α) / (algebraMap K L) (ζ - 1)) j
⊢ (fun x => (algebraMap K L) ζ ^ x * α) i = (fun x => (algebraMap K L) ζ ^ x * α) j
Theorem: KummersLemma.roots_poly
Proof state before:
case neg.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α : ¬α = 0
hζ' : (algebraMap K L) ζ - 1 ≠ 0
i : ℕ
hi : i ∈ ↑(Finset.range ↑p)
j : ℕ
hj : j ∈ ↑(Finset.range ↑p)
e :
  1 - (fun i => (1 - ζ ^ i • α) / (algebraMap K L) (ζ - 1)) i * ((algebraMap K L) ζ - 1) =
    1 - (fun i => (1 - ζ ^ i • α) / (algebraMap K L) (ζ - 1)) j * ((algebraMap K L) ζ - 1)
⊢ (fun x => (algebraMap K L) ζ ^ x * α) i = (fun x => (algebraMap K L) ζ ^ x * α) j
Tactic:
dsimp only at e
Proof state after:
case neg.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α : ¬α = 0
hζ' : (algebraMap K L) ζ - 1 ≠ 0
i : ℕ
hi : i ∈ ↑(Finset.range ↑p)
j : ℕ
hj : j ∈ ↑(Finset.range ↑p)
e :
  1 - (1 - ζ ^ i • α) / (algebraMap K L) (ζ - 1) * ((algebraMap K L) ζ - 1) =
    1 - (1 - ζ ^ j • α) / (algebraMap K L) (ζ - 1) * ((algebraMap K L) ζ - 1)
⊢ (fun x => (algebraMap K L) ζ ^ x * α) i = (fun x => (algebraMap K L) ζ ^ x * α) j
Theorem: KummersLemma.roots_poly
Proof state before:
case neg.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α : ¬α = 0
hζ' : (algebraMap K L) ζ - 1 ≠ 0
i : ℕ
hi : i ∈ ↑(Finset.range ↑p)
j : ℕ
hj : j ∈ ↑(Finset.range ↑p)
e :
  1 - (1 - ζ ^ i • α) / (algebraMap K L) (ζ - 1) * ((algebraMap K L) ζ - 1) =
    1 - (1 - ζ ^ j • α) / (algebraMap K L) (ζ - 1) * ((algebraMap K L) ζ - 1)
⊢ (fun x => (algebraMap K L) ζ ^ x * α) i = (fun x => (algebraMap K L) ζ ^ x * α) j
Tactic:
simpa only [Nat.cast_one, map_sub, map_one, Algebra.smul_def, map_pow,
  div_mul_cancel₀ _ hζ', sub_sub_cancel] using e
Proof state after:
no goals
Theorem: KummersLemma.roots_poly
Proof state before:
case neg.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α : ¬α = 0
hζ' : (algebraMap K L) ζ - 1 ≠ 0
⊢ Multiset.card (map (algebraMap (𝓞 K) L) (poly hp hζ u hcong)).roots ≤
    Multiset.card (Multiset.map (fun i => (1 - ζ ^ i • α) / (algebraMap K L) (ζ - 1)) (Finset.range ↑p).val)
Tactic:
simp only [Finset.range_val, Multiset.card_map, Multiset.card_range]
Proof state after:
case neg.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α : ¬α = 0
hζ' : (algebraMap K L) ζ - 1 ≠ 0
⊢ Multiset.card (map (algebraMap (𝓞 K) L) (poly hp hζ u hcong)).roots ≤ ↑p
Theorem: KummersLemma.roots_poly
Proof state before:
case neg.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α : ¬α = 0
hζ' : (algebraMap K L) ζ - 1 ≠ 0
⊢ Multiset.card (map (algebraMap (𝓞 K) L) (poly hp hζ u hcong)).roots ≤ ↑p
Tactic:
refine (Polynomial.card_roots' _).trans ?_
Proof state after:
case neg.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α : ¬α = 0
hζ' : (algebraMap K L) ζ - 1 ≠ 0
⊢ (map (algebraMap (𝓞 K) L) (poly hp hζ u hcong)).natDegree ≤ ↑p
Theorem: KummersLemma.roots_poly
Proof state before:
case neg.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α : ¬α = 0
hζ' : (algebraMap K L) ζ - 1 ≠ 0
⊢ (map (algebraMap (𝓞 K) L) (poly hp hζ u hcong)).natDegree ≤ ↑p
Tactic:
rw [(monic_poly hp hζ u hcong).natDegree_map, natDegree_poly hp hζ]
Proof state after:
no goals
Theorem: KummersLemma.splits_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
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
⊢ Splits (algebraMap (𝓞 K) L) (poly hp hζ u hcong)
Tactic:
rw [← splits_id_iff_splits, splits_iff_card_roots, roots_poly hp hζ u hcong α e,
  (monic_poly hp hζ u hcong).natDegree_map, natDegree_poly hp hζ,
  Finset.range_val, Multiset.card_map, Multiset.card_range]
Proof state after:
no goals