Theorem: unit_lemma_val_one (FltRegular/NumberTheory/Cyclotomic/GaloisActionOnCyclo.lean)

State before:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
φ : K →+* ℂ
⊢ Complex.abs (φ ((algebraMap (𝓞 K) K) ↑u * (algebraMap (𝓞 K) K) ↑((unitGalConj K p) u)⁻¹)) = 1
Tactic:
rw [map_mul, IsAbsoluteValue.abv_mul Complex.abs, ← zpow_neg_one, NumberField.Units.coe_zpow,
  zpow_neg_one, map_inv₀, ← unitGalConj_spec,
  ← embedding_conj <| zeta_spec p ℚ K]
State after:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
φ : K →+* ℂ
⊢ Complex.abs (φ ((algebraMap (𝓞 K) K) ↑u)) * Complex.abs ((starRingEnd ℂ) (φ ((algebraMap (𝓞 K) K) ↑u)))⁻¹ = 1

State before:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
φ : K →+* ℂ
⊢ Complex.abs (φ ((algebraMap (𝓞 K) K) ↑u)) * Complex.abs ((starRingEnd ℂ) (φ ((algebraMap (𝓞 K) K) ↑u)))⁻¹ = 1
Tactic:
simp only [map_inv₀, Complex.abs_conj]
State after:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
φ : K →+* ℂ
⊢ Complex.abs (φ ((algebraMap (𝓞 K) K) ↑u)) * (Complex.abs (φ ((algebraMap (𝓞 K) K) ↑u)))⁻¹ = 1

State before:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
φ : K →+* ℂ
⊢ Complex.abs (φ ((algebraMap (𝓞 K) K) ↑u)) * (Complex.abs (φ ((algebraMap (𝓞 K) K) ↑u)))⁻¹ = 1
Tactic:
rw [mul_inv_eq_one₀]
State after:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
φ : K →+* ℂ
⊢ Complex.abs (φ ((algebraMap (𝓞 K) K) ↑u)) ≠ 0

State before:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
φ : K →+* ℂ
⊢ Complex.abs (φ ((algebraMap (𝓞 K) K) ↑u)) ≠ 0
Tactic:
intro h
State after:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
φ : K →+* ℂ
h : Complex.abs (φ ((algebraMap (𝓞 K) K) ↑u)) = 0
⊢ False

State before:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
φ : K →+* ℂ
h : Complex.abs (φ ((algebraMap (𝓞 K) K) ↑u)) = 0
⊢ False
Tactic:
simp at h
State after:
no goals