@[instance_reducible]

noncomputable instance Shrink.instLieRingModule_ado (L : Type u_2) {M : Type u_3} [Small.{u, u_3} M] [LieRing L] [AddCommGroup M] [LieRingModule L M] : LieRingModule L (Shrink.{u, u_3} M)

Equations

• Shrink.instLieRingModule_ado L = AddEquiv.lieRingModule L Shrink.addEquiv

instance Shrink.instLieModule_ado (R : Type u_1) (L : Type u_2) {M : Type u_3} [Small.{u, u_3} M] [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : LieModule R L (Shrink.{u, u_3} M)

noncomputable def Shrink.lieModuleEquiv (R : Type u_1) (L : Type u_2) {M : Type u_3} [Small.{u, u_3} M] [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : Shrink.{u, u_3} M ≃ₗ⁅R,L⁆ M

Equations

• Shrink.lieModuleEquiv R L = LinearEquiv.lieModuleEquiv R L (Shrink.linearEquiv R M)

@[simp]

theorem Shrink.isFaithful_iff {R : Type u_1} {L : Type u_2} {M : Type u_3} [Small.{u, u_3} M] [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : LieModule.IsFaithful R L (Shrink.{u, u_3} M) ↔ LieModule.IsFaithful R L M

instance Shrink.instIsFaithful_ado {R : Type u_1} {L : Type u_2} {M : Type u_3} [Small.{u, u_3} M] [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieModule.IsFaithful R L M] : LieModule.IsFaithful R L (Shrink.{u, u_3} M)

@[simp]

theorem Shrink.isNilpotent_iff {L : Type u_2} {M : Type u_3} [Small.{u, u_3} M] [LieRing L] [AddCommGroup M] [LieRingModule L M] : LieModule.IsNilpotent L (Shrink.{u, u_3} M) ↔ LieModule.IsNilpotent L M

instance Shrink.instIsNilpotent_ado {L : Type u_2} {M : Type u_3} [Small.{u, u_3} M] [LieRing L] [AddCommGroup M] [LieRingModule L M] [LieModule.IsNilpotent L M] : LieModule.IsNilpotent L (Shrink.{u, u_3} M)