S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝¹ : Group R
inst✝ : MulAction R M
p : SubMulAction R M
m : { x // x ∈ p }
⊢ (MulAction.stabilizer R m).toSubmonoid = (MulAction.stabilizer R ↑m).toSubmonoid
S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝¹ : Group R
inst✝ : MulAction R M
p : SubMulAction R M
m : { x // x ∈ p }
⊢ MulAction.stabilizer R m = MulAction.stabilizer R ↑m
rw [← Subgroup.toSubmonoid_eq]
no goals
S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝¹ : Group R
inst✝ : MulAction R M
p : SubMulAction R M
m : { x // x ∈ p }
⊢ (MulAction.stabilizer R m).toSubmonoid = (MulAction.stabilizer R ↑m).toSubmonoid
exact stabilizer_of_subMul.submonoid m