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]
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
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