Theorem: unit_inv_conj_not_neg_zeta_runity (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
h : p ≠ 2
u : (𝓞 K)ˣ
n : ℕ
hp : (↑p).Prime
⊢ u * ((unitGalConj K p) u)⁻¹ ≠ -hζ.unit' ^ n
Tactic:
by_contra H
State after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
h : p ≠ 2
u : (𝓞 K)ˣ
n : ℕ
hp : (↑p).Prime
H : u * ((unitGalConj K p) u)⁻¹ = -hζ.unit' ^ n
⊢ False

State before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
h : p ≠ 2
u : (𝓞 K)ˣ
n : ℕ
hp : (↑p).Prime
H : u * ((unitGalConj K p) u)⁻¹ = -hζ.unit' ^ n
⊢ False
Tactic:
have hμ : algebraMap (𝓞 K) (𝓞 K ⧸ I) ((IsPrimitiveRoot.unit' hζ : 𝓞 K) ^ n) = 1 := by
  apply hζ.unit'_coe.eq_one_mod_sub_of_pow
  rw [← pow_mul, mul_comm, pow_mul, hζ.unit'_coe.pow_eq_one, one_pow]
State after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
h : p ≠ 2
u : (𝓞 K)ˣ
n : ℕ
hp : (↑p).Prime
H : u * ((unitGalConj K p) u)⁻¹ = -hζ.unit' ^ n
hμ : (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (↑hζ.unit' ^ n) = 1
⊢ False

State before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
h : p ≠ 2
u : (𝓞 K)ˣ
n : ℕ
hp : (↑p).Prime
H : u * ((unitGalConj K p) u)⁻¹ = -hζ.unit' ^ n
hμ : (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (↑hζ.unit' ^ n) = 1
⊢ False
Tactic:
have hμ' : algebraMap (𝓞 K) (𝓞 K ⧸ I) ((IsPrimitiveRoot.unit' hζ : 𝓞 K) ^ n) = -1 := by
  rw [← neg_eq_iff_eq_neg, ← map_neg, ← Units.val_pow_eq_pow_val, ← Units.val_neg, ← H]
  apply unit_inv_conj_not_neg_zeta_runity_aux hζ u hp
State after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
h : p ≠ 2
u : (𝓞 K)ˣ
n : ℕ
hp : (↑p).Prime
H : u * ((unitGalConj K p) u)⁻¹ = -hζ.unit' ^ n
hμ : (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (↑hζ.unit' ^ n) = 1
hμ' : (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (↑hζ.unit' ^ n) = -1
⊢ False

State before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
h : p ≠ 2
u : (𝓞 K)ˣ
n : ℕ
hp : (↑p).Prime
H : u * ((unitGalConj K p) u)⁻¹ = -hζ.unit' ^ n
hμ : (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (↑hζ.unit' ^ n) = 1
hμ' : (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (↑hζ.unit' ^ n) = -1
⊢ False
Tactic:
haveI := Fact.mk hp
State after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
h : p ≠ 2
u : (𝓞 K)ˣ
n : ℕ
hp : (↑p).Prime
H : u * ((unitGalConj K p) u)⁻¹ = -hζ.unit' ^ n
hμ : (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (↑hζ.unit' ^ n) = 1
hμ' : (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (↑hζ.unit' ^ n) = -1
this : Fact (↑p).Prime
⊢ False

State before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
h : p ≠ 2
u : (𝓞 K)ˣ
n : ℕ
hp : (↑p).Prime
H : u * ((unitGalConj K p) u)⁻¹ = -hζ.unit' ^ n
hμ : (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (↑hζ.unit' ^ n) = 1
hμ' : (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (↑hζ.unit' ^ n) = -1
this : Fact (↑p).Prime
⊢ False
Tactic:
apply hζ.two_not_mem_one_sub_zeta h
State after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
h : p ≠ 2
u : (𝓞 K)ˣ
n : ℕ
hp : (↑p).Prime
H : u * ((unitGalConj K p) u)⁻¹ = -hζ.unit' ^ n
hμ : (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (↑hζ.unit' ^ n) = 1
hμ' : (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (↑hζ.unit' ^ n) = -1
this : Fact (↑p).Prime
⊢ 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
h : p ≠ 2
u : (𝓞 K)ˣ
n : ℕ
hp : (↑p).Prime
H : u * ((unitGalConj K p) u)⁻¹ = -hζ.unit' ^ n
hμ : (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (↑hζ.unit' ^ n) = 1
hμ' : (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (↑hζ.unit' ^ n) = -1
this : Fact (↑p).Prime
⊢ 2 ∈ Ideal.span {↑hζ.unit' - 1}
Tactic:
rw [← Ideal.Quotient.eq_zero_iff_mem, map_two, ← neg_one_eq_one_iff_two_eq_zero, ← hμ', hμ]
State after:
no goals

State before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
h : p ≠ 2
u : (𝓞 K)ˣ
n : ℕ
hp : (↑p).Prime
H : u * ((unitGalConj K p) u)⁻¹ = -hζ.unit' ^ n
⊢ (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (↑hζ.unit' ^ n) = 1
Tactic:
apply hζ.unit'_coe.eq_one_mod_sub_of_pow
State after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
h : p ≠ 2
u : (𝓞 K)ˣ
n : ℕ
hp : (↑p).Prime
H : u * ((unitGalConj K p) u)⁻¹ = -hζ.unit' ^ n
⊢ (↑hζ.unit' ^ n) ^ ↑p = 1

State before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
h : p ≠ 2
u : (𝓞 K)ˣ
n : ℕ
hp : (↑p).Prime
H : u * ((unitGalConj K p) u)⁻¹ = -hζ.unit' ^ n
⊢ (↑hζ.unit' ^ n) ^ ↑p = 1
Tactic:
rw [← pow_mul, mul_comm, pow_mul, hζ.unit'_coe.pow_eq_one, one_pow]
State after:
no goals

State before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
h : p ≠ 2
u : (𝓞 K)ˣ
n : ℕ
hp : (↑p).Prime
H : u * ((unitGalConj K p) u)⁻¹ = -hζ.unit' ^ n
hμ : (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (↑hζ.unit' ^ n) = 1
⊢ (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (↑hζ.unit' ^ n) = -1
Tactic:
rw [← neg_eq_iff_eq_neg, ← map_neg, ← Units.val_pow_eq_pow_val, ← Units.val_neg, ← H]
State after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
h : p ≠ 2
u : (𝓞 K)ˣ
n : ℕ
hp : (↑p).Prime
H : u * ((unitGalConj K p) u)⁻¹ = -hζ.unit' ^ n
hμ : (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (↑hζ.unit' ^ n) = 1
⊢ (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑(u * ((unitGalConj K p) u)⁻¹) = 1

State before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
h : p ≠ 2
u : (𝓞 K)ˣ
n : ℕ
hp : (↑p).Prime
H : u * ((unitGalConj K p) u)⁻¹ = -hζ.unit' ^ n
hμ : (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (↑hζ.unit' ^ n) = 1
⊢ (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑(u * ((unitGalConj K p) u)⁻¹) = 1
Tactic:
apply unit_inv_conj_not_neg_zeta_runity_aux hζ u hp
State after:
no goals