internlm/Lean-Github huggingface dataset:
Theorem: KummersLemma.map_poly_eq_prod
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) = ∏ i ∈ Finset.range ↑p, (X - C (polyRoot hp hζ u hcong α e i))
Tactic:
apply map_injective (algebraMap (𝓞 L) L) 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)
⊢ map (algebraMap (𝓞 L) L) (map (algebraMap (𝓞 K) (𝓞 L)) (poly hp hζ u hcong)) =
    map (algebraMap (𝓞 L) L) (∏ i ∈ Finset.range ↑p, (X - C (polyRoot hp hζ u hcong α e i)))
Theorem: KummersLemma.map_poly_eq_prod
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)
⊢ map (algebraMap (𝓞 L) L) (map (algebraMap (𝓞 K) (𝓞 L)) (poly hp hζ u hcong)) =
    map (algebraMap (𝓞 L) L) (∏ i ∈ Finset.range ↑p, (X - C (polyRoot hp hζ u hcong α e i)))
Tactic:
have : (algebraMap (𝓞 L) L).comp (algebraMap (𝓞 K) (𝓞 L)) = algebraMap (𝓞 K) L := by
  ext; rfl
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)
this : (algebraMap (𝓞 L) L).comp (algebraMap (𝓞 K) (𝓞 L)) = algebraMap (𝓞 K) L
⊢ map (algebraMap (𝓞 L) L) (map (algebraMap (𝓞 K) (𝓞 L)) (poly hp hζ u hcong)) =
    map (algebraMap (𝓞 L) L) (∏ i ∈ Finset.range ↑p, (X - C (polyRoot hp hζ u hcong α e i)))
Theorem: KummersLemma.map_poly_eq_prod
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)
this : (algebraMap (𝓞 L) L).comp (algebraMap (𝓞 K) (𝓞 L)) = algebraMap (𝓞 K) L
⊢ map (algebraMap (𝓞 L) L) (map (algebraMap (𝓞 K) (𝓞 L)) (poly hp hζ u hcong)) =
    map (algebraMap (𝓞 L) L) (∏ i ∈ Finset.range ↑p, (X - C (polyRoot hp hζ u hcong α e i)))
Tactic:
rw [← coe_mapRingHom, map_prod, coe_mapRingHom, map_map, this]
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)
this : (algebraMap (𝓞 L) L).comp (algebraMap (𝓞 K) (𝓞 L)) = algebraMap (𝓞 K) L
⊢ map (algebraMap (𝓞 K) L) (poly hp hζ u hcong) =
    ∏ x ∈ Finset.range ↑p, map (algebraMap (𝓞 L) L) (X - C (polyRoot hp hζ u hcong α e x))
Theorem: KummersLemma.map_poly_eq_prod
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)
this : (algebraMap (𝓞 L) L).comp (algebraMap (𝓞 K) (𝓞 L)) = algebraMap (𝓞 K) L
⊢ map (algebraMap (𝓞 K) L) (poly hp hζ u hcong) =
    ∏ x ∈ Finset.range ↑p, map (algebraMap (𝓞 L) L) (X - C (polyRoot hp hζ u hcong α e x))
Tactic:
rw [eq_prod_roots_of_monic_of_splits_id ((monic_poly hp hζ u hcong).map _)
  ((splits_id_iff_splits _).mpr (splits_poly hp hζ u hcong α e)), roots_poly hp hζ u hcong α e,
  Multiset.map_map]
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)
this : (algebraMap (𝓞 L) L).comp (algebraMap (𝓞 K) (𝓞 L)) = algebraMap (𝓞 K) L
⊢ (Multiset.map ((fun a => X - C a) ∘ fun i => (1 - ζ ^ i • α) / (algebraMap K L) (ζ - 1)) (Finset.range ↑p).val).prod =
    ∏ x ∈ Finset.range ↑p, map (algebraMap (𝓞 L) L) (X - C (polyRoot hp hζ u hcong α e x))
Theorem: KummersLemma.map_poly_eq_prod
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)
this : (algebraMap (𝓞 L) L).comp (algebraMap (𝓞 K) (𝓞 L)) = algebraMap (𝓞 K) L
⊢ (Multiset.map ((fun a => X - C a) ∘ fun i => (1 - ζ ^ i • α) / (algebraMap K L) (ζ - 1)) (Finset.range ↑p).val).prod =
    ∏ x ∈ Finset.range ↑p, map (algebraMap (𝓞 L) L) (X - C (polyRoot hp hζ u hcong α e x))
Tactic:
simp only [Polynomial.map_sub, map_X, map_C]
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)
this : (algebraMap (𝓞 L) L).comp (algebraMap (𝓞 K) (𝓞 L)) = algebraMap (𝓞 K) L
⊢ (Multiset.map ((fun a => X - C a) ∘ fun i => (1 - ζ ^ i • α) / (algebraMap K L) (ζ - 1)) (Finset.range ↑p).val).prod =
    ∏ x ∈ Finset.range ↑p, (X - C ((algebraMap (𝓞 L) L) (polyRoot hp hζ u hcong α e x)))
Theorem: KummersLemma.map_poly_eq_prod
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)
this : (algebraMap (𝓞 L) L).comp (algebraMap (𝓞 K) (𝓞 L)) = algebraMap (𝓞 K) L
⊢ (Multiset.map ((fun a => X - C a) ∘ fun i => (1 - ζ ^ i • α) / (algebraMap K L) (ζ - 1)) (Finset.range ↑p).val).prod =
    ∏ x ∈ Finset.range ↑p, (X - C ((algebraMap (𝓞 L) L) (polyRoot hp hζ u hcong α e x)))
Tactic:
rfl
Proof state after:
no goals
Theorem: KummersLemma.map_poly_eq_prod
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 (𝓞 L) L).comp (algebraMap (𝓞 K) (𝓞 L)) = algebraMap (𝓞 K) L
Tactic:
ext
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)
x✝ : 𝓞 K
⊢ ((algebraMap (𝓞 L) L).comp (algebraMap (𝓞 K) (𝓞 L))) x✝ = (algebraMap (𝓞 K) L) x✝
Theorem: KummersLemma.map_poly_eq_prod
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)
x✝ : 𝓞 K
⊢ ((algebraMap (𝓞 L) L).comp (algebraMap (𝓞 K) (𝓞 L))) x✝ = (algebraMap (𝓞 K) L) x✝
Tactic:
rfl
Proof state after:
no goals
Theorem: KummersLemma.isIntegralClosure_of_isScalarTower
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
R : Type u_2
A : Type u_3
K : Type u_4
L : Type u_5
B : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing A
inst✝¹² : CommRing K
inst✝¹¹ : CommRing L
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra R K
inst✝⁸ : Algebra A K
inst✝⁷ : Algebra R L
inst✝⁶ : Algebra B L
inst✝⁵ : Algebra A L
inst✝⁴ : Algebra R A
inst✝³ : IsScalarTower R A K
inst✝² : IsScalarTower R A L
inst✝¹ : IsIntegralClosure A R K
inst✝ : IsIntegralClosure B R L
x : L
⊢ IsIntegral A x ↔ ∃ y, (algebraMap B L) y = x
Tactic:
refine Iff.trans ?_ (IsIntegralClosure.isIntegral_iff (R := R) (A := B) (B := 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
R : Type u_2
A : Type u_3
K : Type u_4
L : Type u_5
B : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing A
inst✝¹² : CommRing K
inst✝¹¹ : CommRing L
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra R K
inst✝⁸ : Algebra A K
inst✝⁷ : Algebra R L
inst✝⁶ : Algebra B L
inst✝⁵ : Algebra A L
inst✝⁴ : Algebra R A
inst✝³ : IsScalarTower R A K
inst✝² : IsScalarTower R A L
inst✝¹ : IsIntegralClosure A R K
inst✝ : IsIntegralClosure B R L
x : L
⊢ IsIntegral A x ↔ IsIntegral R x
Theorem: KummersLemma.isIntegralClosure_of_isScalarTower
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
R : Type u_2
A : Type u_3
K : Type u_4
L : Type u_5
B : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing A
inst✝¹² : CommRing K
inst✝¹¹ : CommRing L
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra R K
inst✝⁸ : Algebra A K
inst✝⁷ : Algebra R L
inst✝⁶ : Algebra B L
inst✝⁵ : Algebra A L
inst✝⁴ : Algebra R A
inst✝³ : IsScalarTower R A K
inst✝² : IsScalarTower R A L
inst✝¹ : IsIntegralClosure A R K
inst✝ : IsIntegralClosure B R L
x : L
⊢ IsIntegral A x ↔ IsIntegral R x
Tactic:
have := (IsIntegralClosure.isIntegral_algebra R (A := A) 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
R : Type u_2
A : Type u_3
K : Type u_4
L : Type u_5
B : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing A
inst✝¹² : CommRing K
inst✝¹¹ : CommRing L
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra R K
inst✝⁸ : Algebra A K
inst✝⁷ : Algebra R L
inst✝⁶ : Algebra B L
inst✝⁵ : Algebra A L
inst✝⁴ : Algebra R A
inst✝³ : IsScalarTower R A K
inst✝² : IsScalarTower R A L
inst✝¹ : IsIntegralClosure A R K
inst✝ : IsIntegralClosure B R L
x : L
this : Algebra.IsIntegral R A
⊢ IsIntegral A x ↔ IsIntegral R x
Theorem: KummersLemma.isIntegralClosure_of_isScalarTower
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
R : Type u_2
A : Type u_3
K : Type u_4
L : Type u_5
B : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing A
inst✝¹² : CommRing K
inst✝¹¹ : CommRing L
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra R K
inst✝⁸ : Algebra A K
inst✝⁷ : Algebra R L
inst✝⁶ : Algebra B L
inst✝⁵ : Algebra A L
inst✝⁴ : Algebra R A
inst✝³ : IsScalarTower R A K
inst✝² : IsScalarTower R A L
inst✝¹ : IsIntegralClosure A R K
inst✝ : IsIntegralClosure B R L
x : L
this : Algebra.IsIntegral R A
⊢ IsIntegral A x ↔ IsIntegral R x
Tactic:
exact ⟨isIntegral_trans x, IsIntegral.tower_top⟩
Proof state after:
no goals
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) = map (algebraMap (𝓞 K) K) (poly hp hζ u hcong)
Tactic:
have : IsIntegral K (polyRoot hp hζ u hcong α e i : L) :=
  IsIntegral.tower_top (polyRoot hp hζ u hcong α e i).prop
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)
i : ℕ
this : IsIntegral K ↑(polyRoot hp hζ u hcong α e i)
⊢ 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:
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 : ℕ
this : IsIntegral K ↑(polyRoot hp hζ u hcong α e i)
⊢ minpoly K ↑(polyRoot hp hζ u hcong α e i) = map (algebraMap (𝓞 K) K) (poly hp hζ u hcong)
Tactic:
apply eq_of_monic_of_associated (minpoly.monic this) ((monic_poly hp hζ u hcong).map _)
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)
i : ℕ
this : IsIntegral K ↑(polyRoot hp hζ u hcong α e i)
⊢ Associated (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:
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 : ℕ
this : IsIntegral K ↑(polyRoot hp hζ u hcong α e i)
⊢ Associated (minpoly K ↑(polyRoot hp hζ u hcong α e i)) (map (algebraMap (𝓞 K) K) (poly hp hζ u hcong))
Tactic:
refine Irreducible.associated_of_dvd (minpoly.irreducible this)
  (irreducible_map_poly hp hζ u hcong hu) (minpoly.dvd _ _ ?_)
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)
i : ℕ
this : IsIntegral K ↑(polyRoot hp hζ u hcong α e i)
⊢ (aeval ↑(polyRoot hp hζ u hcong α e i)) (map (algebraMap (𝓞 K) K) (poly hp hζ u hcong)) = 0
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 : ℕ
this : IsIntegral K ↑(polyRoot hp hζ u hcong α e i)
⊢ (aeval ↑(polyRoot hp hζ u hcong α e i)) (map (algebraMap (𝓞 K) K) (poly hp hζ u hcong)) = 0
Tactic:
rw [aeval_def, eval₂_map, ← IsScalarTower.algebraMap_eq, ← aeval_def]
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)
i : ℕ
this : IsIntegral K ↑(polyRoot hp hζ u hcong α e i)
⊢ (aeval ↑(polyRoot hp hζ u hcong α e i)) (poly hp hζ u hcong) = 0
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 : ℕ
this : IsIntegral K ↑(polyRoot hp hζ u hcong α e i)
⊢ (aeval ↑(polyRoot hp hζ u hcong α e i)) (poly hp hζ u hcong) = 0
Tactic:
exact aeval_poly hp hζ u hcong α e i
Proof state after:
no goals
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]
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 ↑(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 ↑(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 IsIntegral.tower_top (polyRoot hp hζ u hcong α e i).prop
Proof state after:
no goals