internlm/Lean-Github huggingface dataset:
Theorem: Spts.not_two
Proof state before:
case inr
a : ℤ√(-3)
him : a.im ≠ 0
⊢ a.re * a.re - -3 * a.im * a.im ≠ 2
Tactic:
apply ne_of_gt
Proof state after:
case inr.h
a : ℤ√(-3)
him : a.im ≠ 0
⊢ 2 < a.re * a.re - -3 * a.im * a.im
Theorem: Spts.not_two
Proof state before:
case inr.h
a : ℤ√(-3)
him : a.im ≠ 0
⊢ 2 < a.re * a.re - -3 * a.im * a.im
Tactic:
apply lt_add_of_nonneg_of_lt (mul_self_nonneg a.re)
Proof state after:
case inr.h
a : ℤ√(-3)
him : a.im ≠ 0
⊢ 2 < -(-3 * a.im * a.im)
Theorem: Spts.not_two
Proof state before:
case inr.h
a : ℤ√(-3)
him : a.im ≠ 0
⊢ 2 < -(-3 * a.im * a.im)
Tactic:
rw [← Int.add_one_le_iff]
Proof state after:
case inr.h
a : ℤ√(-3)
him : a.im ≠ 0
⊢ 2 + 1 ≤ -(-3 * a.im * a.im)
Theorem: Spts.not_two
Proof state before:
case inr.h
a : ℤ√(-3)
him : a.im ≠ 0
⊢ 2 + 1 ≤ -(-3 * a.im * a.im)
Tactic:
rw [mul_assoc, neg_mul_eq_neg_mul, neg_neg]
Proof state after:
case inr.h
a : ℤ√(-3)
him : a.im ≠ 0
⊢ 2 + 1 ≤ 3 * (a.im * a.im)
Theorem: Spts.not_two
Proof state before:
case inr.h
a : ℤ√(-3)
him : a.im ≠ 0
⊢ 2 + 1 ≤ 3 * (a.im * a.im)
Tactic:
refine' le_mul_of_one_le_right zero_lt_three.le _
Proof state after:
case inr.h
a : ℤ√(-3)
him : a.im ≠ 0
⊢ 1 ≤ a.im * a.im
Theorem: Spts.not_two
Proof state before:
case inr.h
a : ℤ√(-3)
him : a.im ≠ 0
⊢ 1 ≤ a.im * a.im
Tactic:
rwa [← Int.sub_one_lt_iff, sub_self, mul_self_pos]
Proof state after:
no goals
Theorem: Spts.four
Proof state before:
p : ℤ√(-3)
hfour : p.norm = 4
hq✝ : p.im ≠ 0
hq : p.im ^ 2 = 1
⊢ p.re ^ 2 = 1 ∧ p.im ^ 2 = 1
Tactic:
refine' ⟨_, hq⟩
Proof state after:
p : ℤ√(-3)
hfour : p.norm = 4
hq✝ : p.im ≠ 0
hq : p.im ^ 2 = 1
⊢ p.re ^ 2 = 1
Theorem: Spts.four
Proof state before:
p : ℤ√(-3)
hfour : p.norm = 4
hq✝ : p.im ≠ 0
hq : p.im ^ 2 = 1
⊢ p.re ^ 2 = 1
Tactic:
calc
  p.re ^ 2 = p.re ^ 2 + 3 * p.im ^ 2 - 3 := by simp [hq]
  _ = p.norm - 3 := by
    rw [Zsqrtd.norm_def]
    ring
  _ = 1 := by
    rw [hfour]
    norm_num
Proof state after:
no goals
Theorem: Spts.four
Proof state before:
p : ℤ√(-3)
hfour : p.norm = 4
hq : p.im ≠ 0
this : p.re ^ 2 = 1 ∧ p.im ^ 2 = 1
⊢ p.im ^ 2 = 1 → |p.im| = 1
Tactic:
intro h
Proof state after:
p : ℤ√(-3)
hfour : p.norm = 4
hq : p.im ≠ 0
this : p.re ^ 2 = 1 ∧ p.im ^ 2 = 1
h : p.im ^ 2 = 1
⊢ |p.im| = 1
Theorem: Spts.four
Proof state before:
p : ℤ√(-3)
hfour : p.norm = 4
hq : p.im ≠ 0
this : p.re ^ 2 = 1 ∧ p.im ^ 2 = 1
h : p.im ^ 2 = 1
⊢ |p.im| = 1
Tactic:
rwa [← sq_eq_sq (abs_nonneg (_ : ℤ)) zero_le_one, one_pow, sq_abs]
Proof state after:
no goals
Theorem: Spts.four
Proof state before:
p : ℤ√(-3)
hfour : p.norm = 4
hq : p.im ≠ 0
⊢ p.im ^ 2 = 1
Tactic:
apply le_antisymm
Proof state after:
case a
p : ℤ√(-3)
hfour : p.norm = 4
hq : p.im ≠ 0
⊢ p.im ^ 2 ≤ 1

case a
p : ℤ√(-3)
hfour : p.norm = 4
hq : p.im ≠ 0
⊢ 1 ≤ p.im ^ 2
Theorem: Spts.four
Proof state before:
case a
p : ℤ√(-3)
hfour : p.norm = 4
hq : p.im ≠ 0
⊢ p.im ^ 2 ≤ 1
Tactic:
contrapose! hfour with hq'
Proof state after:
case a
p : ℤ√(-3)
hq : p.im ≠ 0
hq' : 1 < p.im ^ 2
⊢ p.norm ≠ 4
Theorem: Spts.four
Proof state before:
case a
p : ℤ√(-3)
hq : p.im ≠ 0
hq' : 1 < p.im ^ 2
⊢ p.norm ≠ 4
Tactic:
apply ne_of_gt
Proof state after:
case a.h
p : ℤ√(-3)
hq : p.im ≠ 0
hq' : 1 < p.im ^ 2
⊢ 4 < p.norm
Theorem: Spts.four
Proof state before:
case a.h
p : ℤ√(-3)
hq : p.im ≠ 0
hq' : 1 < p.im ^ 2
⊢ 4 < p.norm
Tactic:
rw [← Int.add_one_le_iff] at hq'
Proof state after:
case a.h
p : ℤ√(-3)
hq : p.im ≠ 0
hq' : 1 + 1 ≤ p.im ^ 2
⊢ 4 < p.norm
Theorem: Spts.four
Proof state before:
case a.h
p : ℤ√(-3)
hq : p.im ≠ 0
hq' : 1 + 1 ≤ p.im ^ 2
⊢ 4 < p.norm
Tactic:
calc
  4 < 3 * 2 := by norm_num
  _ ≤ 3 * p.im ^ 2 := (Int.mul_le_mul_of_nonneg_left hq' (by norm_num))
  _ ≤ p.re ^ 2 + 3 * p.im ^ 2 := (le_add_of_nonneg_left (pow_two_nonneg p.re))
  _ = p.norm := by
    rw [Zsqrtd.norm_def]
    ring
Proof state after:
no goals
Theorem: Spts.four
Proof state before:
p : ℤ√(-3)
hq : p.im ≠ 0
hq' : 1 + 1 ≤ p.im ^ 2
⊢ 4 < 3 * 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: Spts.four
Proof state before:
p : ℤ√(-3)
hq : p.im ≠ 0
hq' : 1 + 1 ≤ p.im ^ 2
⊢ 0 ≤ 3
Tactic:
norm_num
Proof state after:
no goals
Theorem: Spts.four
Proof state before:
p : ℤ√(-3)
hq : p.im ≠ 0
hq' : 1 + 1 ≤ p.im ^ 2
⊢ p.re ^ 2 + 3 * p.im ^ 2 = p.norm
Tactic:
rw [Zsqrtd.norm_def]
Proof state after:
p : ℤ√(-3)
hq : p.im ≠ 0
hq' : 1 + 1 ≤ p.im ^ 2
⊢ p.re ^ 2 + 3 * p.im ^ 2 = p.re * p.re - -3 * p.im * p.im
Theorem: Spts.four
Proof state before:
p : ℤ√(-3)
hq : p.im ≠ 0
hq' : 1 + 1 ≤ p.im ^ 2
⊢ p.re ^ 2 + 3 * p.im ^ 2 = p.re * p.re - -3 * p.im * p.im
Tactic:
ring
Proof state after:
no goals
Theorem: Spts.four
Proof state before:
case a
p : ℤ√(-3)
hfour : p.norm = 4
hq : p.im ≠ 0
⊢ 1 ≤ p.im ^ 2
Tactic:
rw [← Int.sub_one_lt_iff, sub_self]
Proof state after:
case a
p : ℤ√(-3)
hfour : p.norm = 4
hq : p.im ≠ 0
⊢ 0 < p.im ^ 2
Theorem: Spts.four
Proof state before:
case a
p : ℤ√(-3)
hfour : p.norm = 4
hq : p.im ≠ 0
⊢ 0 < p.im ^ 2
Tactic:
exact sq_pos_of_ne_zero hq
Proof state after:
no goals
Theorem: Spts.four
Proof state before:
p : ℤ√(-3)
hfour : p.norm = 4
hq✝ : p.im ≠ 0
hq : p.im ^ 2 = 1
⊢ p.re ^ 2 = p.re ^ 2 + 3 * p.im ^ 2 - 3
Tactic:
simp [hq]
Proof state after:
no goals
Theorem: Spts.four
Proof state before:
p : ℤ√(-3)
hfour : p.norm = 4
hq✝ : p.im ≠ 0
hq : p.im ^ 2 = 1
⊢ p.re ^ 2 + 3 * p.im ^ 2 - 3 = p.norm - 3
Tactic:
rw [Zsqrtd.norm_def]
Proof state after:
p : ℤ√(-3)
hfour : p.norm = 4
hq✝ : p.im ≠ 0
hq : p.im ^ 2 = 1
⊢ p.re ^ 2 + 3 * p.im ^ 2 - 3 = p.re * p.re - -3 * p.im * p.im - 3
Theorem: Spts.four
Proof state before:
p : ℤ√(-3)
hfour : p.norm = 4
hq✝ : p.im ≠ 0
hq : p.im ^ 2 = 1
⊢ p.re ^ 2 + 3 * p.im ^ 2 - 3 = p.re * p.re - -3 * p.im * p.im - 3
Tactic:
ring
Proof state after:
no goals
Theorem: Spts.four
Proof state before:
p : ℤ√(-3)
hfour : p.norm = 4
hq✝ : p.im ≠ 0
hq : p.im ^ 2 = 1
⊢ p.norm - 3 = 1
Tactic:
rw [hfour]
Proof state after:
p : ℤ√(-3)
hfour : p.norm = 4
hq✝ : p.im ≠ 0
hq : p.im ^ 2 = 1
⊢ 4 - 3 = 1
Theorem: Spts.four
Proof state before:
p : ℤ√(-3)
hfour : p.norm = 4
hq✝ : p.im ≠ 0
hq : p.im ^ 2 = 1
⊢ 4 - 3 = 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: Spts.four_of_coprime
Proof state before:
p : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hfour : p.norm = 4
⊢ |p.re| = 1 ∧ |p.im| = 1
Tactic:
apply Spts.four hfour
Proof state after:
p : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hfour : p.norm = 4
⊢ p.im ≠ 0
Theorem: Spts.four_of_coprime
Proof state before:
p : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hfour : p.norm = 4
⊢ p.im ≠ 0
Tactic:
rintro him
Proof state after:
p : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hfour : p.norm = 4
him : p.im = 0
⊢ False
Theorem: Spts.four_of_coprime
Proof state before:
p : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hfour : p.norm = 4
him : p.im = 0
⊢ False
Tactic:
rw [him, isCoprime_zero_right, Int.isUnit_iff_abs_eq] at hcoprime
Proof state after:
p : ℤ√(-3)
hcoprime : |p.re| = 1
hfour : p.norm = 4
him : p.im = 0
⊢ False
Theorem: Spts.four_of_coprime
Proof state before:
p : ℤ√(-3)
hcoprime : |p.re| = 1
hfour : p.norm = 4
him : p.im = 0
⊢ False
Tactic:
rw [Zsqrtd.norm_def, him, MulZeroClass.mul_zero, sub_zero, ← sq, ← sq_abs, hcoprime] at hfour
Proof state after:
p : ℤ√(-3)
hcoprime : |p.re| = 1
hfour : 1 ^ 2 = 4
him : p.im = 0
⊢ False
Theorem: Spts.four_of_coprime
Proof state before:
p : ℤ√(-3)
hcoprime : |p.re| = 1
hfour : 1 ^ 2 = 4
him : p.im = 0
⊢ False
Tactic:
norm_num at hfour
Proof state after:
no goals
Theorem: false_of_zeta_sub_one_pow_dvd_sub_one_of_pow_ne
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
inst✝⁴ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : 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.27748
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u✝))
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
⊢ False
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
inst✝⁴ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : 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.27748
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u✝))
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑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 }
⊢ False
Theorem: false_of_zeta_sub_one_pow_dvd_sub_one_of_pow_ne
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
inst✝⁴ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : 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.27748
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u✝))
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑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 }
⊢ False
Tactic:
let L := AdjoinRoot (Polynomial.X ^ (p : ℕ) - Polynomial.C (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
inst✝⁴ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : 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.27748
inst✝³ : Field L✝
inst✝² : Algebra K L✝
inst✝¹ : FiniteDimensional K L✝
inst✝ : IsSplittingField K L✝ (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u✝))
σ : L✝ ≃ₐ[K] L✝
hσ : ∀ (x : L✝ ≃ₐ[K] L✝), x ∈ Subgroup.zpowers σ
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑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 }
L : Type u_1 := AdjoinRoot (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
⊢ False
Theorem: false_of_zeta_sub_one_pow_dvd_sub_one_of_pow_ne
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
inst✝⁴ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : 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.27748
inst✝³ : Field L✝
inst✝² : Algebra K L✝
inst✝¹ : FiniteDimensional K L✝
inst✝ : IsSplittingField K L✝ (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u✝))
σ : L✝ ≃ₐ[K] L✝
hσ : ∀ (x : L✝ ≃ₐ[K] L✝), x ∈ Subgroup.zpowers σ
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑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 }
L : Type u_1 := AdjoinRoot (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
⊢ False
Tactic:
haveI := isSplittingField_AdjoinRoot_X_pow_sub_C ⟨ζ, (mem_primitiveRoots p.pos).mpr hζ⟩
  (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
inst✝⁴ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : 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.27748
inst✝³ : Field L✝
inst✝² : Algebra K L✝
inst✝¹ : FiniteDimensional K L✝
inst✝ : IsSplittingField K L✝ (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u✝))
σ : L✝ ≃ₐ[K] L✝
hσ : ∀ (x : L✝ ≃ₐ[K] L✝), x ∈ Subgroup.zpowers σ
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑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 }
L : Type u_1 := AdjoinRoot (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
this : IsSplittingField K (AdjoinRoot (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
⊢ False
Theorem: false_of_zeta_sub_one_pow_dvd_sub_one_of_pow_ne
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
inst✝⁴ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : 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.27748
inst✝³ : Field L✝
inst✝² : Algebra K L✝
inst✝¹ : FiniteDimensional K L✝
inst✝ : IsSplittingField K L✝ (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u✝))
σ : L✝ ≃ₐ[K] L✝
hσ : ∀ (x : L✝ ≃ₐ[K] L✝), x ∈ Subgroup.zpowers σ
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑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 }
L : Type u_1 := AdjoinRoot (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
this : IsSplittingField K (AdjoinRoot (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
⊢ False
Tactic:
haveI := isGalois_of_isSplittingField_X_pow_sub_C ⟨ζ, (mem_primitiveRoots p.pos).mpr hζ⟩
  (X_pow_sub_C_irreducible_of_prime hpri.out hu) 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
inst✝⁴ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : 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.27748
inst✝³ : Field L✝
inst✝² : Algebra K L✝
inst✝¹ : FiniteDimensional K L✝
inst✝ : IsSplittingField K L✝ (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u✝))
σ : L✝ ≃ₐ[K] L✝
hσ : ∀ (x : L✝ ≃ₐ[K] L✝), x ∈ Subgroup.zpowers σ
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑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 }
L : Type u_1 := AdjoinRoot (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
this✝ : IsSplittingField K (AdjoinRoot (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
this : IsGalois K L
⊢ False
Theorem: false_of_zeta_sub_one_pow_dvd_sub_one_of_pow_ne
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
inst✝⁴ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : 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.27748
inst✝³ : Field L✝
inst✝² : Algebra K L✝
inst✝¹ : FiniteDimensional K L✝
inst✝ : IsSplittingField K L✝ (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u✝))
σ : L✝ ≃ₐ[K] L✝
hσ : ∀ (x : L✝ ≃ₐ[K] L✝), x ∈ Subgroup.zpowers σ
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑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 }
L : Type u_1 := AdjoinRoot (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
this✝ : IsSplittingField K (AdjoinRoot (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
this : IsGalois K L
⊢ False
Tactic:
have := Polynomial.IsSplittingField.finiteDimensional L
  (Polynomial.X ^ (p : ℕ) - Polynomial.C (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
inst✝⁴ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : 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.27748
inst✝³ : Field L✝
inst✝² : Algebra K L✝
inst✝¹ : FiniteDimensional K L✝
inst✝ : IsSplittingField K L✝ (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u✝))
σ : L✝ ≃ₐ[K] L✝
hσ : ∀ (x : L✝ ≃ₐ[K] L✝), x ∈ Subgroup.zpowers σ
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑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 }
L : Type u_1 := AdjoinRoot (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
this✝¹ : IsSplittingField K (AdjoinRoot (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
this✝ : IsGalois K L
this : FiniteDimensional K L
⊢ False
Theorem: false_of_zeta_sub_one_pow_dvd_sub_one_of_pow_ne
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
inst✝⁴ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : 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.27748
inst✝³ : Field L✝
inst✝² : Algebra K L✝
inst✝¹ : FiniteDimensional K L✝
inst✝ : IsSplittingField K L✝ (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u✝))
σ : L✝ ≃ₐ[K] L✝
hσ : ∀ (x : L✝ ≃ₐ[K] L✝), x ∈ Subgroup.zpowers σ
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑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 }
L : Type u_1 := AdjoinRoot (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
this✝¹ : IsSplittingField K (AdjoinRoot (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
this✝ : IsGalois K L
this : FiniteDimensional K L
⊢ False
Tactic:
have := isCyclic_of_isSplittingField_X_pow_sub_C ⟨ζ, (mem_primitiveRoots p.pos).mpr hζ⟩
    (X_pow_sub_C_irreducible_of_prime hpri.out hu) 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
inst✝⁴ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : 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.27748
inst✝³ : Field L✝
inst✝² : Algebra K L✝
inst✝¹ : FiniteDimensional K L✝
inst✝ : IsSplittingField K L✝ (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u✝))
σ : L✝ ≃ₐ[K] L✝
hσ : ∀ (x : L✝ ≃ₐ[K] L✝), x ∈ Subgroup.zpowers σ
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑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 }
L : Type u_1 := AdjoinRoot (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
this✝² : IsSplittingField K (AdjoinRoot (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
this✝¹ : IsGalois K L
this✝ : FiniteDimensional K L
this : IsCyclic (L ≃ₐ[K] L)
⊢ False
Theorem: false_of_zeta_sub_one_pow_dvd_sub_one_of_pow_ne
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
inst✝⁴ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : 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.27748
inst✝³ : Field L✝
inst✝² : Algebra K L✝
inst✝¹ : FiniteDimensional K L✝
inst✝ : IsSplittingField K L✝ (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u✝))
σ : L✝ ≃ₐ[K] L✝
hσ : ∀ (x : L✝ ≃ₐ[K] L✝), x ∈ Subgroup.zpowers σ
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑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 }
L : Type u_1 := AdjoinRoot (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
this✝² : IsSplittingField K (AdjoinRoot (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
this✝¹ : IsGalois K L
this✝ : FiniteDimensional K L
this : IsCyclic (L ≃ₐ[K] L)
⊢ False
Tactic:
have : CharZero L := charZero_of_injective_algebraMap (algebraMap K L).injective
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
inst✝⁴ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : 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.27748
inst✝³ : Field L✝
inst✝² : Algebra K L✝
inst✝¹ : FiniteDimensional K L✝
inst✝ : IsSplittingField K L✝ (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u✝))
σ : L✝ ≃ₐ[K] L✝
hσ : ∀ (x : L✝ ≃ₐ[K] L✝), x ∈ Subgroup.zpowers σ
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑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 }
L : Type u_1 := AdjoinRoot (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
this✝³ : IsSplittingField K (AdjoinRoot (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
this✝² : IsGalois K L
this✝¹ : FiniteDimensional K L
this✝ : IsCyclic (L ≃ₐ[K] L)
this : CharZero L
⊢ False