no goals
α : Type ?u.391210
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝² : Monoid M
inst✝¹ : Group G
inst✝ : Ring R
a : M
x y : Mˣ
h : SemiconjBy a ↑x ↑y
n : ℕ
⊢ SemiconjBy a ↑(x ^ ↑n) ↑(y ^ ↑n)
simp only [zpow_ofNat, Units.val_pow_eq_pow_val, h, pow_right]
no goals
α : Type ?u.391210
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝² : Monoid M
inst✝¹ : Group G
inst✝ : Ring R
a : M
x y : Mˣ
h : SemiconjBy a ↑x ↑y
n : ℕ
⊢ SemiconjBy a ↑(x ^ -[n+1]) ↑(y ^ -[n+1])
simp only [zpow_negSucc, Units.val_pow_eq_pow_val, units_inv_right, h, pow_right]