Documentation

Ado.ForMathlib.LieModuleSubsingleton

instance LieModule.instIsFaithfulOfSubsingleton_ado {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] [Subsingleton L] :