Theorem: KummersLemma.separable_poly_aux (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
α : 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)
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

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)]
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

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)
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))

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
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))

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
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)

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)
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)

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
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)

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
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)

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
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)

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
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)

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
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)

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
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 * ⟨α, ⋯⟩

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
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 * ⟨α, ⋯⟩)

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]
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) * α

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ζ']
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) * α

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
State after:
no goals

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)
State after:
no goals

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 ?_ ?_ ?_
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

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]
State after:
no goals

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]
State after:
no goals

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
State after:
no goals

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
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)

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]
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))

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
State after:
no goals

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]
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)

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
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

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
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)

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]
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)

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
State after:
no goals