R : Type u_2
L : Type u_1
M : Type ?u.56361
M' : Type ?u.56364
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
H : LieSubalgebra R L
x y : L
hx : x ∈ normalizer H
hy : y ∈ H
⊢ ⁅y, x⁆ ∈ H
R : Type u_2
L : Type u_1
M : Type ?u.56361
M' : Type ?u.56364
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
H : LieSubalgebra R L
x y : L
hx : x ∈ normalizer H
hy : y ∈ H
⊢ ⁅x, y⁆ ∈ H
rw [← lie_skew, neg_mem_iff (G := L)]
no goals
R : Type u_2
L : Type u_1
M : Type ?u.56361
M' : Type ?u.56364
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
H : LieSubalgebra R L
x y : L
hx : x ∈ normalizer H
hy : y ∈ H
⊢ ⁅y, x⁆ ∈ H
exact hx ⟨y, hy⟩