Documentation

Ado.ForMathlib.LieModuleRestr

source
@[simp]
theorem LieSubmodule.restr_top {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] (L' : LieSubalgebra R L) :
⊤.restr L' = ⊤
source
@[simp]
theorem LieSubmodule.restr_bot {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] (L' : LieSubalgebra R L) :
⊥.restr L' = ⊥