G : Type ?u.5843
G' : Type ?u.5846
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.5855
inst✝² : AddGroup A
M : Type u_1
S : Type u_2
inst✝¹ : DivInvMonoid M
inst✝ : SetLike S M
hSM : SubgroupClass S M
H K : S
x : M
hx : x ∈ K
n : ℕ
⊢ x ^ n ∈ K
G : Type ?u.5843
G' : Type ?u.5846
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.5855
inst✝² : AddGroup A
M : Type u_1
S : Type u_2
inst✝¹ : DivInvMonoid M
inst✝ : SetLike S M
hSM : SubgroupClass S M
H K : S
x : M
hx : x ∈ K
n : ℕ
⊢ x ^ ↑n ∈ K
rw [zpow_ofNat]
no goals
G : Type ?u.5843
G' : Type ?u.5846
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.5855
inst✝² : AddGroup A
M : Type u_1
S : Type u_2
inst✝¹ : DivInvMonoid M
inst✝ : SetLike S M
hSM : SubgroupClass S M
H K : S
x : M
hx : x ∈ K
n : ℕ
⊢ x ^ n ∈ K
exact pow_mem hx n
G : Type ?u.5843
G' : Type ?u.5846
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.5855
inst✝² : AddGroup A
M : Type u_1
S : Type u_2
inst✝¹ : DivInvMonoid M
inst✝ : SetLike S M
hSM : SubgroupClass S M
H K : S
x : M
hx : x ∈ K
n : ℕ
⊢ (x ^ (n + 1))⁻¹ ∈ K
G : Type ?u.5843
G' : Type ?u.5846
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.5855
inst✝² : AddGroup A
M : Type u_1
S : Type u_2
inst✝¹ : DivInvMonoid M
inst✝ : SetLike S M
hSM : SubgroupClass S M
H K : S
x : M
hx : x ∈ K
n : ℕ
⊢ x ^ -[n+1] ∈ K
rw [zpow_negSucc]
no goals
G : Type ?u.5843
G' : Type ?u.5846
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.5855
inst✝² : AddGroup A
M : Type u_1
S : Type u_2
inst✝¹ : DivInvMonoid M
inst✝ : SetLike S M
hSM : SubgroupClass S M
H K : S
x : M
hx : x ∈ K
n : ℕ
⊢ (x ^ (n + 1))⁻¹ ∈ K
exact inv_mem (pow_mem hx n.succ)