Theorem: IsPrimitiveRoot.two_not_mem_one_sub_zeta (FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean)

State before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : Fact (↑p).Prime
h : p ≠ 2
⊢ 2 ∉ Ideal.span {↑hζ.unit' - 1}
Tactic:
have hpm := hζ.p_mem_one_sub_zeta
State after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : Fact (↑p).Prime
h : p ≠ 2
hpm : ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}
⊢ 2 ∉ Ideal.span {↑hζ.unit' - 1}

State before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : Fact (↑p).Prime
h : p ≠ 2
hpm : ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}
⊢ 2 ∉ Ideal.span {↑hζ.unit' - 1}
Tactic:
obtain ⟨k, hk⟩ := hp.1.odd_of_ne_two (norm_cast_ne_two h)
State after:
case intro
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : Fact (↑p).Prime
h : p ≠ 2
hpm : ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}
k : ℕ
hk : ↑p = 2 * k + 1
⊢ 2 ∉ Ideal.span {↑hζ.unit' - 1}

State before:
case intro
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : Fact (↑p).Prime
h : p ≠ 2
hpm : ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}
k : ℕ
hk : ↑p = 2 * k + 1
⊢ 2 ∉ Ideal.span {↑hζ.unit' - 1}
Tactic:
apply_fun (fun n : ℕ => (n : 𝓞 K)) at hk
State after:
case intro
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : Fact (↑p).Prime
h : p ≠ 2
hpm : ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}
k : ℕ
hk : ↑↑p = ↑(2 * k + 1)
⊢ 2 ∉ Ideal.span {↑hζ.unit' - 1}

State before:
case intro
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : Fact (↑p).Prime
h : p ≠ 2
hpm : ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}
k : ℕ
hk : ↑↑p = ↑(2 * k + 1)
⊢ 2 ∉ Ideal.span {↑hζ.unit' - 1}
Tactic:
rw [Nat.cast_add, Nat.cast_mul, Nat.cast_two, Nat.cast_one, add_comm] at hk
State after:
case intro
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : Fact (↑p).Prime
h : p ≠ 2
hpm : ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}
k : ℕ
hk : ↑↑p = 1 + 2 * ↑k
⊢ 2 ∉ Ideal.span {↑hζ.unit' - 1}

State before:
case intro
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : Fact (↑p).Prime
h : p ≠ 2
hpm : ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}
k : ℕ
hk : ↑↑p = 1 + 2 * ↑k
⊢ 2 ∉ Ideal.span {↑hζ.unit' - 1}
Tactic:
intro h2m
State after:
case intro
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : Fact (↑p).Prime
h : p ≠ 2
hpm : ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}
k : ℕ
hk : ↑↑p = 1 + 2 * ↑k
h2m : 2 ∈ Ideal.span {↑hζ.unit' - 1}
⊢ False

State before:
case intro
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : Fact (↑p).Prime
h : p ≠ 2
hpm : ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}
k : ℕ
hk : ↑↑p = 1 + 2 * ↑k
h2m : 2 ∈ Ideal.span {↑hζ.unit' - 1}
⊢ False
Tactic:
have := Ideal.sub_mem I hpm (Ideal.mul_mem_right (↑k) I h2m)
State after:
case intro
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : Fact (↑p).Prime
h : p ≠ 2
hpm : ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}
k : ℕ
hk : ↑↑p = 1 + 2 * ↑k
h2m : 2 ∈ Ideal.span {↑hζ.unit' - 1}
this : ↑↑p - 2 * ↑k ∈ Ideal.span {↑hζ.unit' - 1}
⊢ False

State before:
case intro
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : Fact (↑p).Prime
h : p ≠ 2
hpm : ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}
k : ℕ
hk : ↑↑p = 1 + 2 * ↑k
h2m : 2 ∈ Ideal.span {↑hζ.unit' - 1}
this : ↑↑p - 2 * ↑k ∈ Ideal.span {↑hζ.unit' - 1}
⊢ False
Tactic:
rw [sub_eq_of_eq_add hk] at this
State after:
case intro
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : Fact (↑p).Prime
h : p ≠ 2
hpm : ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}
k : ℕ
hk : ↑↑p = 1 + 2 * ↑k
h2m : 2 ∈ Ideal.span {↑hζ.unit' - 1}
this : 1 ∈ Ideal.span {↑hζ.unit' - 1}
⊢ False

State before:
case intro
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : Fact (↑p).Prime
h : p ≠ 2
hpm : ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}
k : ℕ
hk : ↑↑p = 1 + 2 * ↑k
h2m : 2 ∈ Ideal.span {↑hζ.unit' - 1}
this : 1 ∈ Ideal.span {↑hζ.unit' - 1}
⊢ False
Tactic:
exact hζ.isPrime_one_sub_zeta.ne_top (Ideal.eq_top_of_isUnit_mem I this isUnit_one)
State after:
no goals