no goals
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
p : ℕ
hp : Fact (Nat.Prime p)
hg : x ^ p = 1
hg1 : x ≠ 1
⊢ ¬IsFixedPt (fun x_1 => x * x_1) 1
rwa [IsFixedPt, mul_one]