@[simp]
theorem
Prod.lieModule_ker_eq
{R : Type u_1}
{L : Type u_2}
{M : Type u_3}
{N : Type u_4}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[AddCommGroup N]
[Module R M]
[Module R N]
[LieRingModule L M]
[LieRingModule L N]
[LieModule R L M]
[LieModule R L N]
:
@[simp]
theorem
LieSubalgebra.ker_eq
{R : Type u_1}
{L : Type u_2}
{M : Type u_3}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
(L' : LieSubalgebra R L)
:
LieIdeal.toLieSubalgebra R (↥L') (LieModule.ker R (↥L') M) = comap L'.incl (LieIdeal.toLieSubalgebra R L (LieModule.ker R L M))
@[simp]
theorem
LieIdeal.ker_eq
{R : Type u_1}
{L : Type u_2}
{M : Type u_3}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
(I : LieIdeal R L)
: