internlm/Lean-Github huggingface dataset:
Theorem: aux
Proof state before:
case h.e'_3.e_f.h
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
t : ℕ
l : 𝓞 K
f : Fin t → ℤ
μ : K
hμ : IsPrimitiveRoot μ ↑p
h :
  ∑ x : Fin t, f x • (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (⟨μ, ⋯⟩ ^ ↑x) =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) l
x : Fin t
this : ⟨μ, ⋯⟩ ^ ↑p = 1
⊢ ↑(f x) = f x • (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (⟨μ, ⋯⟩ ^ ↑x)
Tactic:
have := hζ.unit'_coe.eq_one_mod_sub_of_pow this
Proof state after:
case h.e'_3.e_f.h
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
t : ℕ
l : 𝓞 K
f : Fin t → ℤ
μ : K
hμ : IsPrimitiveRoot μ ↑p
h :
  ∑ x : Fin t, f x • (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (⟨μ, ⋯⟩ ^ ↑x) =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) l
x : Fin t
this✝ : ⟨μ, ⋯⟩ ^ ↑p = 1
this : (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ⟨μ, ⋯⟩ = 1
⊢ ↑(f x) = f x • (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (⟨μ, ⋯⟩ ^ ↑x)
Theorem: aux
Proof state before:
case h.e'_3.e_f.h
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
t : ℕ
l : 𝓞 K
f : Fin t → ℤ
μ : K
hμ : IsPrimitiveRoot μ ↑p
h :
  ∑ x : Fin t, f x • (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (⟨μ, ⋯⟩ ^ ↑x) =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) l
x : Fin t
this✝ : ⟨μ, ⋯⟩ ^ ↑p = 1
this : (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ⟨μ, ⋯⟩ = 1
⊢ ↑(f x) = f x • (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (⟨μ, ⋯⟩ ^ ↑x)
Tactic:
simp only [map_pow (algebraMap (𝓞 K) (𝓞 K ⧸ I)), this, one_pow, zsmul_one]
Proof state after:
no goals
Theorem: aux
Proof state before:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
t : ℕ
l : 𝓞 K
f : Fin t → ℤ
μ : K
hμ : IsPrimitiveRoot μ ↑p
h :
  ∑ x : Fin t, f x • (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (⟨μ, ⋯⟩ ^ ↑x) =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) l
x : Fin t
⊢ ⟨μ, ⋯⟩ ^ ↑p = 1
Tactic:
ext
Proof state after:
case a
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
t : ℕ
l : 𝓞 K
f : Fin t → ℤ
μ : K
hμ : IsPrimitiveRoot μ ↑p
h :
  ∑ x : Fin t, f x • (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (⟨μ, ⋯⟩ ^ ↑x) =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) l
x : Fin t
⊢ ↑(⟨μ, ⋯⟩ ^ ↑p) = ↑1
Theorem: aux
Proof state before:
case a
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
t : ℕ
l : 𝓞 K
f : Fin t → ℤ
μ : K
hμ : IsPrimitiveRoot μ ↑p
h :
  ∑ x : Fin t, f x • (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (⟨μ, ⋯⟩ ^ ↑x) =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) l
x : Fin t
⊢ ↑(⟨μ, ⋯⟩ ^ ↑p) = ↑1
Tactic:
push_cast
Proof state after:
case a
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
t : ℕ
l : 𝓞 K
f : Fin t → ℤ
μ : K
hμ : IsPrimitiveRoot μ ↑p
h :
  ∑ x : Fin t, f x • (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (⟨μ, ⋯⟩ ^ ↑x) =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) l
x : Fin t
⊢ μ ^ ↑p = 1
Theorem: aux
Proof state before:
case a
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
t : ℕ
l : 𝓞 K
f : Fin t → ℤ
μ : K
hμ : IsPrimitiveRoot μ ↑p
h :
  ∑ x : Fin t, f x • (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (⟨μ, ⋯⟩ ^ ↑x) =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) l
x : Fin t
⊢ μ ^ ↑p = 1
Tactic:
exact hμ.pow_eq_one
Proof state after:
no goals
Theorem: IsPrimitiveRoot.p_mem_one_sub_zeta
Proof state before:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
hp : Fact (↑p).Prime
⊢ ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}
Tactic:
classical
have key : _ = (p : 𝓞 K) := @Polynomial.eval_one_cyclotomic_prime _ _ _ hp
rw [cyclotomic_eq_prod_X_sub_primitiveRoots hζ.unit'_coe, eval_prod] at key
simp only [eval_sub, eval_X, eval_C] at key
have : {↑hζ.unit'} ⊆ primitiveRoots p (𝓞 K) := by simpa using hζ.unit'_coe
rw [← Finset.prod_sdiff this, Finset.prod_singleton] at key
rw [← key]
have := (Ideal.neg_mem_iff I).mpr (Ideal.subset_span (Set.mem_singleton ζ1))
rw [neg_sub] at this
exact Ideal.mul_mem_left _ _ this
Proof state after:
no goals
Theorem: IsPrimitiveRoot.p_mem_one_sub_zeta
Proof state before:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
hp : Fact (↑p).Prime
⊢ ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}
Tactic:
have key : _ = (p : 𝓞 K) := @Polynomial.eval_one_cyclotomic_prime _ _ _ hp
Proof state after:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
hp : Fact (↑p).Prime
key : eval 1 (cyclotomic (↑p) (𝓞 K)) = ↑↑p
⊢ ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}
Theorem: IsPrimitiveRoot.p_mem_one_sub_zeta
Proof state before:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
hp : Fact (↑p).Prime
key : eval 1 (cyclotomic (↑p) (𝓞 K)) = ↑↑p
⊢ ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}
Tactic:
rw [cyclotomic_eq_prod_X_sub_primitiveRoots hζ.unit'_coe, eval_prod] at key
Proof state after:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
hp : Fact (↑p).Prime
key : ∏ j ∈ primitiveRoots (↑p) (𝓞 K), eval 1 (X - C j) = ↑↑p
⊢ ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}
Theorem: IsPrimitiveRoot.p_mem_one_sub_zeta
Proof state before:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
hp : Fact (↑p).Prime
key : ∏ j ∈ primitiveRoots (↑p) (𝓞 K), eval 1 (X - C j) = ↑↑p
⊢ ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}
Tactic:
simp only [eval_sub, eval_X, eval_C] at key
Proof state after:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
hp : Fact (↑p).Prime
key : ∏ x ∈ primitiveRoots (↑p) (𝓞 K), (1 - x) = ↑↑p
⊢ ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}
Theorem: IsPrimitiveRoot.p_mem_one_sub_zeta
Proof state before:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
hp : Fact (↑p).Prime
key : ∏ x ∈ primitiveRoots (↑p) (𝓞 K), (1 - x) = ↑↑p
⊢ ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}
Tactic:
have : {↑hζ.unit'} ⊆ primitiveRoots p (𝓞 K) := by simpa using hζ.unit'_coe
Proof state after:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
hp : Fact (↑p).Prime
key : ∏ x ∈ primitiveRoots (↑p) (𝓞 K), (1 - x) = ↑↑p
this : {↑hζ.unit'} ⊆ primitiveRoots (↑p) (𝓞 K)
⊢ ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}
Theorem: IsPrimitiveRoot.p_mem_one_sub_zeta
Proof state before:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
hp : Fact (↑p).Prime
key : ∏ x ∈ primitiveRoots (↑p) (𝓞 K), (1 - x) = ↑↑p
this : {↑hζ.unit'} ⊆ primitiveRoots (↑p) (𝓞 K)
⊢ ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}
Tactic:
rw [← Finset.prod_sdiff this, Finset.prod_singleton] at key
Proof state after:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
hp : Fact (↑p).Prime
key : (∏ x ∈ primitiveRoots (↑p) (𝓞 K) \ {↑hζ.unit'}, (1 - x)) * (1 - ↑hζ.unit') = ↑↑p
this : {↑hζ.unit'} ⊆ primitiveRoots (↑p) (𝓞 K)
⊢ ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}
Theorem: IsPrimitiveRoot.p_mem_one_sub_zeta
Proof state before:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
hp : Fact (↑p).Prime
key : (∏ x ∈ primitiveRoots (↑p) (𝓞 K) \ {↑hζ.unit'}, (1 - x)) * (1 - ↑hζ.unit') = ↑↑p
this : {↑hζ.unit'} ⊆ primitiveRoots (↑p) (𝓞 K)
⊢ ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}
Tactic:
rw [← key]
Proof state after:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
hp : Fact (↑p).Prime
key : (∏ x ∈ primitiveRoots (↑p) (𝓞 K) \ {↑hζ.unit'}, (1 - x)) * (1 - ↑hζ.unit') = ↑↑p
this : {↑hζ.unit'} ⊆ primitiveRoots (↑p) (𝓞 K)
⊢ (∏ x ∈ primitiveRoots (↑p) (𝓞 K) \ {↑hζ.unit'}, (1 - x)) * (1 - ↑hζ.unit') ∈ Ideal.span {↑hζ.unit' - 1}
Theorem: IsPrimitiveRoot.p_mem_one_sub_zeta
Proof state before:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
hp : Fact (↑p).Prime
key : (∏ x ∈ primitiveRoots (↑p) (𝓞 K) \ {↑hζ.unit'}, (1 - x)) * (1 - ↑hζ.unit') = ↑↑p
this : {↑hζ.unit'} ⊆ primitiveRoots (↑p) (𝓞 K)
⊢ (∏ x ∈ primitiveRoots (↑p) (𝓞 K) \ {↑hζ.unit'}, (1 - x)) * (1 - ↑hζ.unit') ∈ Ideal.span {↑hζ.unit' - 1}
Tactic:
have := (Ideal.neg_mem_iff I).mpr (Ideal.subset_span (Set.mem_singleton ζ1))
Proof state after:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
hp : Fact (↑p).Prime
key : (∏ x ∈ primitiveRoots (↑p) (𝓞 K) \ {↑hζ.unit'}, (1 - x)) * (1 - ↑hζ.unit') = ↑↑p
this✝ : {↑hζ.unit'} ⊆ primitiveRoots (↑p) (𝓞 K)
this : -(↑hζ.unit' - 1) ∈ Ideal.span {↑hζ.unit' - 1}
⊢ (∏ x ∈ primitiveRoots (↑p) (𝓞 K) \ {↑hζ.unit'}, (1 - x)) * (1 - ↑hζ.unit') ∈ Ideal.span {↑hζ.unit' - 1}
Theorem: IsPrimitiveRoot.p_mem_one_sub_zeta
Proof state before:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
hp : Fact (↑p).Prime
key : (∏ x ∈ primitiveRoots (↑p) (𝓞 K) \ {↑hζ.unit'}, (1 - x)) * (1 - ↑hζ.unit') = ↑↑p
this✝ : {↑hζ.unit'} ⊆ primitiveRoots (↑p) (𝓞 K)
this : -(↑hζ.unit' - 1) ∈ Ideal.span {↑hζ.unit' - 1}
⊢ (∏ x ∈ primitiveRoots (↑p) (𝓞 K) \ {↑hζ.unit'}, (1 - x)) * (1 - ↑hζ.unit') ∈ Ideal.span {↑hζ.unit' - 1}
Tactic:
rw [neg_sub] at this
Proof state after:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
hp : Fact (↑p).Prime
key : (∏ x ∈ primitiveRoots (↑p) (𝓞 K) \ {↑hζ.unit'}, (1 - x)) * (1 - ↑hζ.unit') = ↑↑p
this✝ : {↑hζ.unit'} ⊆ primitiveRoots (↑p) (𝓞 K)
this : 1 - ↑hζ.unit' ∈ Ideal.span {↑hζ.unit' - 1}
⊢ (∏ x ∈ primitiveRoots (↑p) (𝓞 K) \ {↑hζ.unit'}, (1 - x)) * (1 - ↑hζ.unit') ∈ Ideal.span {↑hζ.unit' - 1}
Theorem: IsPrimitiveRoot.p_mem_one_sub_zeta
Proof state before:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
hp : Fact (↑p).Prime
key : (∏ x ∈ primitiveRoots (↑p) (𝓞 K) \ {↑hζ.unit'}, (1 - x)) * (1 - ↑hζ.unit') = ↑↑p
this✝ : {↑hζ.unit'} ⊆ primitiveRoots (↑p) (𝓞 K)
this : 1 - ↑hζ.unit' ∈ Ideal.span {↑hζ.unit' - 1}
⊢ (∏ x ∈ primitiveRoots (↑p) (𝓞 K) \ {↑hζ.unit'}, (1 - x)) * (1 - ↑hζ.unit') ∈ Ideal.span {↑hζ.unit' - 1}
Tactic:
exact Ideal.mul_mem_left _ _ this
Proof state after:
no goals
Theorem: IsPrimitiveRoot.p_mem_one_sub_zeta
Proof state before:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
hp : Fact (↑p).Prime
key : ∏ x ∈ primitiveRoots (↑p) (𝓞 K), (1 - x) = ↑↑p
⊢ {↑hζ.unit'} ⊆ primitiveRoots (↑p) (𝓞 K)
Tactic:
simpa using hζ.unit'_coe
Proof state after:
no goals
Theorem: roots_of_unity_in_cyclo_aux
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
x : K
n l : ℕ
hl : l ∈ n.divisors
hx : IsIntegral ℤ x
hhl : (cyclotomic l (𝓞 K)).IsRoot ⟨x, hx⟩
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
⊢ l ∣ 2 * ↑p
Tactic:
by_contra h
Proof state after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
x : K
n l : ℕ
hl : l ∈ n.divisors
hx : IsIntegral ℤ x
hhl : (cyclotomic l (𝓞 K)).IsRoot ⟨x, hx⟩
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
h : ¬l ∣ 2 * ↑p
⊢ False
Theorem: roots_of_unity_in_cyclo_aux
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
x : K
n l : ℕ
hl : l ∈ n.divisors
hx : IsIntegral ℤ x
hhl : (cyclotomic l (𝓞 K)).IsRoot ⟨x, hx⟩
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
h : ¬l ∣ 2 * ↑p
⊢ False
Tactic:
have hpl' : IsPrimitiveRoot (⟨x, hx⟩ : R) l := by
  have nezero : NeZero (l : 𝓞 K) := by
    refine' ⟨fun hzero => _⟩
    simp only [Nat.cast_eq_zero] at hzero
    simp [hzero] at hl
  rw [isRoot_cyclotomic_iff.symm]
  apply hhl
Proof state after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
x : K
n l : ℕ
hl : l ∈ n.divisors
hx : IsIntegral ℤ x
hhl : (cyclotomic l (𝓞 K)).IsRoot ⟨x, hx⟩
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
h : ¬l ∣ 2 * ↑p
hpl' : IsPrimitiveRoot ⟨x, hx⟩ l
⊢ False
Theorem: roots_of_unity_in_cyclo_aux
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
x : K
n l : ℕ
hl : l ∈ n.divisors
hx : IsIntegral ℤ x
hhl : (cyclotomic l (𝓞 K)).IsRoot ⟨x, hx⟩
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
h : ¬l ∣ 2 * ↑p
hpl' : IsPrimitiveRoot ⟨x, hx⟩ l
⊢ False
Tactic:
have hpl : IsPrimitiveRoot x l := by
  have : (algebraMap R K) ⟨x, hx⟩ = x := by rfl
  have h4 := IsPrimitiveRoot.map_of_injective hpl' (f := algebraMap (𝓞 K) K); rw [← this]
  apply h4
  apply IsFractionRing.injective
Proof state after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
x : K
n l : ℕ
hl : l ∈ n.divisors
hx : IsIntegral ℤ x
hhl : (cyclotomic l (𝓞 K)).IsRoot ⟨x, hx⟩
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
h : ¬l ∣ 2 * ↑p
hpl' : IsPrimitiveRoot ⟨x, hx⟩ l
hpl : IsPrimitiveRoot x l
⊢ False
Theorem: roots_of_unity_in_cyclo_aux
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
x : K
n l : ℕ
hl : l ∈ n.divisors
hx : IsIntegral ℤ x
hhl : (cyclotomic l (𝓞 K)).IsRoot ⟨x, hx⟩
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
h : ¬l ∣ 2 * ↑p
hpl' : IsPrimitiveRoot ⟨x, hx⟩ l
hpl : IsPrimitiveRoot x l
⊢ False
Tactic:
have KEY := contains_two_primitive_roots hpl hζ
Proof state after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
x : K
n l : ℕ
hl : l ∈ n.divisors
hx : IsIntegral ℤ x
hhl : (cyclotomic l (𝓞 K)).IsRoot ⟨x, hx⟩
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
h : ¬l ∣ 2 * ↑p
hpl' : IsPrimitiveRoot ⟨x, hx⟩ l
hpl : IsPrimitiveRoot x l
KEY : (lcm l ↑p).totient ≤ FiniteDimensional.finrank ℚ K
⊢ False
Theorem: roots_of_unity_in_cyclo_aux
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
x : K
n l : ℕ
hl : l ∈ n.divisors
hx : IsIntegral ℤ x
hhl : (cyclotomic l (𝓞 K)).IsRoot ⟨x, hx⟩
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
h : ¬l ∣ 2 * ↑p
hpl' : IsPrimitiveRoot ⟨x, hx⟩ l
hpl : IsPrimitiveRoot x l
KEY : (lcm l ↑p).totient ≤ FiniteDimensional.finrank ℚ K
⊢ False
Tactic:
have hirr : Irreducible (cyclotomic p ℚ) := cyclotomic.irreducible_rat p.prop
Proof state after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
x : K
n l : ℕ
hl : l ∈ n.divisors
hx : IsIntegral ℤ x
hhl : (cyclotomic l (𝓞 K)).IsRoot ⟨x, hx⟩
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
h : ¬l ∣ 2 * ↑p
hpl' : IsPrimitiveRoot ⟨x, hx⟩ l
hpl : IsPrimitiveRoot x l
KEY : (lcm l ↑p).totient ≤ FiniteDimensional.finrank ℚ K
hirr : Irreducible (cyclotomic ↑p ℚ)
⊢ False
Theorem: roots_of_unity_in_cyclo_aux
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
x : K
n l : ℕ
hl : l ∈ n.divisors
hx : IsIntegral ℤ x
hhl : (cyclotomic l (𝓞 K)).IsRoot ⟨x, hx⟩
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
h : ¬l ∣ 2 * ↑p
hpl' : IsPrimitiveRoot ⟨x, hx⟩ l
hpl : IsPrimitiveRoot x l
KEY : (lcm l ↑p).totient ≤ FiniteDimensional.finrank ℚ K
hirr : Irreducible (cyclotomic ↑p ℚ)
⊢ False
Tactic:
have hrank := IsCyclotomicExtension.finrank K hirr
Proof state after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
x : K
n l : ℕ
hl : l ∈ n.divisors
hx : IsIntegral ℤ x
hhl : (cyclotomic l (𝓞 K)).IsRoot ⟨x, hx⟩
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
h : ¬l ∣ 2 * ↑p
hpl' : IsPrimitiveRoot ⟨x, hx⟩ l
hpl : IsPrimitiveRoot x l
KEY : (lcm l ↑p).totient ≤ FiniteDimensional.finrank ℚ K
hirr : Irreducible (cyclotomic ↑p ℚ)
hrank : FiniteDimensional.finrank ℚ K = (↑p).totient
⊢ False
Theorem: roots_of_unity_in_cyclo_aux
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
x : K
n l : ℕ
hl : l ∈ n.divisors
hx : IsIntegral ℤ x
hhl : (cyclotomic l (𝓞 K)).IsRoot ⟨x, hx⟩
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
h : ¬l ∣ 2 * ↑p
hpl' : IsPrimitiveRoot ⟨x, hx⟩ l
hpl : IsPrimitiveRoot x l
KEY : (lcm l ↑p).totient ≤ FiniteDimensional.finrank ℚ K
hirr : Irreducible (cyclotomic ↑p ℚ)
hrank : FiniteDimensional.finrank ℚ K = (↑p).totient
⊢ False
Tactic:
rw [hrank] at KEY
Proof state after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
x : K
n l : ℕ
hl : l ∈ n.divisors
hx : IsIntegral ℤ x
hhl : (cyclotomic l (𝓞 K)).IsRoot ⟨x, hx⟩
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
h : ¬l ∣ 2 * ↑p
hpl' : IsPrimitiveRoot ⟨x, hx⟩ l
hpl : IsPrimitiveRoot x l
KEY : (lcm l ↑p).totient ≤ (↑p).totient
hirr : Irreducible (cyclotomic ↑p ℚ)
hrank : FiniteDimensional.finrank ℚ K = (↑p).totient
⊢ False
Theorem: roots_of_unity_in_cyclo_aux
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
x : K
n l : ℕ
hl : l ∈ n.divisors
hx : IsIntegral ℤ x
hhl : (cyclotomic l (𝓞 K)).IsRoot ⟨x, hx⟩
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
h : ¬l ∣ 2 * ↑p
hpl' : IsPrimitiveRoot ⟨x, hx⟩ l
hpl : IsPrimitiveRoot x l
KEY : (lcm l ↑p).totient ≤ (↑p).totient
hirr : Irreducible (cyclotomic ↑p ℚ)
hrank : FiniteDimensional.finrank ℚ K = (↑p).totient
⊢ False
Tactic:
have pdivlcm : (p : ℕ) ∣ lcm l p := dvd_lcm_right l ↑p
Proof state after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
x : K
n l : ℕ
hl : l ∈ n.divisors
hx : IsIntegral ℤ x
hhl : (cyclotomic l (𝓞 K)).IsRoot ⟨x, hx⟩
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
h : ¬l ∣ 2 * ↑p
hpl' : IsPrimitiveRoot ⟨x, hx⟩ l
hpl : IsPrimitiveRoot x l
KEY : (lcm l ↑p).totient ≤ (↑p).totient
hirr : Irreducible (cyclotomic ↑p ℚ)
hrank : FiniteDimensional.finrank ℚ K = (↑p).totient
pdivlcm : ↑p ∣ lcm l ↑p
⊢ False
Theorem: roots_of_unity_in_cyclo_aux
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
x : K
n l : ℕ
hl : l ∈ n.divisors
hx : IsIntegral ℤ x
hhl : (cyclotomic l (𝓞 K)).IsRoot ⟨x, hx⟩
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
h : ¬l ∣ 2 * ↑p
hpl' : IsPrimitiveRoot ⟨x, hx⟩ l
hpl : IsPrimitiveRoot x l
KEY : (lcm l ↑p).totient ≤ (↑p).totient
hirr : Irreducible (cyclotomic ↑p ℚ)
hrank : FiniteDimensional.finrank ℚ K = (↑p).totient
pdivlcm : ↑p ∣ lcm l ↑p
⊢ False
Tactic:
cases' pdivlcm with pdivlcm_w pdivlcm_h
Proof state after:
case intro
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
x : K
n l : ℕ
hl : l ∈ n.divisors
hx : IsIntegral ℤ x
hhl : (cyclotomic l (𝓞 K)).IsRoot ⟨x, hx⟩
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
h : ¬l ∣ 2 * ↑p
hpl' : IsPrimitiveRoot ⟨x, hx⟩ l
hpl : IsPrimitiveRoot x l
KEY : (lcm l ↑p).totient ≤ (↑p).totient
hirr : Irreducible (cyclotomic ↑p ℚ)
hrank : FiniteDimensional.finrank ℚ K = (↑p).totient
pdivlcm_w : ℕ
pdivlcm_h : lcm l ↑p = ↑p * pdivlcm_w
⊢ False
Theorem: roots_of_unity_in_cyclo_aux
Proof state before:
case intro
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
x : K
n l : ℕ
hl : l ∈ n.divisors
hx : IsIntegral ℤ x
hhl : (cyclotomic l (𝓞 K)).IsRoot ⟨x, hx⟩
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
h : ¬l ∣ 2 * ↑p
hpl' : IsPrimitiveRoot ⟨x, hx⟩ l
hpl : IsPrimitiveRoot x l
KEY : (lcm l ↑p).totient ≤ (↑p).totient
hirr : Irreducible (cyclotomic ↑p ℚ)
hrank : FiniteDimensional.finrank ℚ K = (↑p).totient
pdivlcm_w : ℕ
pdivlcm_h : lcm l ↑p = ↑p * pdivlcm_w
⊢ False
Tactic:
have ineq1 := Nat.totient_super_multiplicative (p : ℕ) pdivlcm_w
Proof state after:
case intro
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
x : K
n l : ℕ
hl : l ∈ n.divisors
hx : IsIntegral ℤ x
hhl : (cyclotomic l (𝓞 K)).IsRoot ⟨x, hx⟩
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
h : ¬l ∣ 2 * ↑p
hpl' : IsPrimitiveRoot ⟨x, hx⟩ l
hpl : IsPrimitiveRoot x l
KEY : (lcm l ↑p).totient ≤ (↑p).totient
hirr : Irreducible (cyclotomic ↑p ℚ)
hrank : FiniteDimensional.finrank ℚ K = (↑p).totient
pdivlcm_w : ℕ
pdivlcm_h : lcm l ↑p = ↑p * pdivlcm_w
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (↑p * pdivlcm_w).totient
⊢ False
Theorem: roots_of_unity_in_cyclo_aux
Proof state before:
case intro
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
x : K
n l : ℕ
hl : l ∈ n.divisors
hx : IsIntegral ℤ x
hhl : (cyclotomic l (𝓞 K)).IsRoot ⟨x, hx⟩
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
h : ¬l ∣ 2 * ↑p
hpl' : IsPrimitiveRoot ⟨x, hx⟩ l
hpl : IsPrimitiveRoot x l
KEY : (lcm l ↑p).totient ≤ (↑p).totient
hirr : Irreducible (cyclotomic ↑p ℚ)
hrank : FiniteDimensional.finrank ℚ K = (↑p).totient
pdivlcm_w : ℕ
pdivlcm_h : lcm l ↑p = ↑p * pdivlcm_w
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (↑p * pdivlcm_w).totient
⊢ False
Tactic:
rw [← pdivlcm_h] at ineq1
Proof state after:
case intro
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
x : K
n l : ℕ
hl : l ∈ n.divisors
hx : IsIntegral ℤ x
hhl : (cyclotomic l (𝓞 K)).IsRoot ⟨x, hx⟩
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
h : ¬l ∣ 2 * ↑p
hpl' : IsPrimitiveRoot ⟨x, hx⟩ l
hpl : IsPrimitiveRoot x l
KEY : (lcm l ↑p).totient ≤ (↑p).totient
hirr : Irreducible (cyclotomic ↑p ℚ)
hrank : FiniteDimensional.finrank ℚ K = (↑p).totient
pdivlcm_w : ℕ
pdivlcm_h : lcm l ↑p = ↑p * pdivlcm_w
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
⊢ False
Theorem: roots_of_unity_in_cyclo_aux
Proof state before:
case intro
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
x : K
n l : ℕ
hl : l ∈ n.divisors
hx : IsIntegral ℤ x
hhl : (cyclotomic l (𝓞 K)).IsRoot ⟨x, hx⟩
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
h : ¬l ∣ 2 * ↑p
hpl' : IsPrimitiveRoot ⟨x, hx⟩ l
hpl : IsPrimitiveRoot x l
KEY : (lcm l ↑p).totient ≤ (↑p).totient
hirr : Irreducible (cyclotomic ↑p ℚ)
hrank : FiniteDimensional.finrank ℚ K = (↑p).totient
pdivlcm_w : ℕ
pdivlcm_h : lcm l ↑p = ↑p * pdivlcm_w
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
⊢ False
Tactic:
have KEY3 := (mul_le_iff_le_one_right (Nat.totient_pos.2 p.prop)).mp (le_trans ineq1 KEY)
Proof state after:
case intro
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
x : K
n l : ℕ
hl : l ∈ n.divisors
hx : IsIntegral ℤ x
hhl : (cyclotomic l (𝓞 K)).IsRoot ⟨x, hx⟩
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
h : ¬l ∣ 2 * ↑p
hpl' : IsPrimitiveRoot ⟨x, hx⟩ l
hpl : IsPrimitiveRoot x l
KEY : (lcm l ↑p).totient ≤ (↑p).totient
hirr : Irreducible (cyclotomic ↑p ℚ)
hrank : FiniteDimensional.finrank ℚ K = (↑p).totient
pdivlcm_w : ℕ
pdivlcm_h : lcm l ↑p = ↑p * pdivlcm_w
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
⊢ False