@[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] : LieModule.ker R L (M × N) = LieModule.ker R L M ⊓ LieModule.ker 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) : ↑R (↥L') (LieModule.ker R (↥L') M) = comap L'.incl (↑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) : LieModule.ker R (↥I) M = comap I.incl (LieModule.ker R L M)

theorem LieModule.isTrivial_iff_ker (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] : IsTrivial L M ↔ LieModule.ker R L M = ⊤