case h.h
R : Type u
L : Type v
M : Type w
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
A : Type v
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
⊢ ↑(↑(ad R A) a) b = ↑((LinearMap.mulLeft R - LinearMap.mulRight R) a) b
R : Type u
L : Type v
M : Type w
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
A : Type v
inst✝¹ : Ring A
inst✝ : Algebra R A
⊢ ↑(ad R A) = LinearMap.mulLeft R - LinearMap.mulRight R
ext (a b)
no goals
case h.h
R : Type u
L : Type v
M : Type w
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
A : Type v
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
⊢ ↑(↑(ad R A) a) b = ↑((LinearMap.mulLeft R - LinearMap.mulRight R) a) b
simp [LieRing.of_associative_ring_bracket]