rw [eq_comm, hx.mul_left_injective.eq_iff]
p : ℕ+
K : Type ?u.152499
inst✝³ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
S : Type u_1
inst✝ : CommRing S
x : S
hx : IsUnit x
y : S
⊢ 1 * x = y * x ↔ y = 1
no goals