@[instance_reducible]

instance PUnit.instBracket_ado {L : Type u_2} : Bracket L PUnit.{u_3 + 1}

Equations

• PUnit.instBracket_ado = { bracket := fun (x : L) (x_1 : PUnit.{?u.1 + 1}) => PUnit.unit }

@[simp]

theorem PUnit.bracket_eq {L : Type u_2} (x : L) (m : PUnit.{u_3 + 1}) : ⁅x, m⁆ = unit

@[instance_reducible]

instance PUnit.instLieRingModule_ado {L : Type u_2} [LieRing L] : LieRingModule L PUnit.{u_3 + 1}

Equations

• PUnit.instLieRingModule_ado = { toBracket := PUnit.instBracket_ado, add_lie := ⋯, lie_add := ⋯, leibniz_lie := ⋯ }

instance PUnit.instLieModule_ado {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] : LieModule R L PUnit.{u_3 + 1}