rw [mul_inv_self]
case a
p : ℕ+
K✝ : Type ?u.244158
inst✝⁵ : Field K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p
inst✝⁴ : NumberField K✝
inst✝³ : IsCyclotomicExtension {p} ℚ K✝
K : Type u_1
A : Type u_2
inst✝² : Field K
inst✝¹ : SetLike A K
inst✝ : SubsemiringClass A K
S : A
s : (↥S)ˣ
⊢ ↑↑(s * s⁻¹) = 1
case a
p : ℕ+
K✝ : Type ?u.244158
inst✝⁵ : Field K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p
inst✝⁴ : NumberField K✝
inst✝³ : IsCyclotomicExtension {p} ℚ K✝
K : Type u_1
A : Type u_2
inst✝² : Field K
inst✝¹ : SetLike A K
inst✝ : SubsemiringClass A K
S : A
s : (↥S)ˣ
⊢ ↑↑1 = 1