simp_rw [NumberField.Units.coe_zpow]
case h
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ x y i : ℤ
⊢ (galConj K p) ((algebraMap (𝓞 K) K) ↑(hζ.unit' ^ i)) = ((algebraMap (𝓞 K) K) ↑(hζ.unit' ^ i))⁻¹ ∨ y = 0
case h
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ x y i : ℤ
⊢ (galConj K p) ((algebraMap (𝓞 K) K) ↑hζ.unit' ^ i) = ((algebraMap (𝓞 K) K) ↑hζ.unit' ^ i)⁻¹ ∨ y = 0