Theorems · Definition · nonassociative algebras

RightPreLieAlgebra.mk.noConfusion

{R : Type u_1} →
  {inst : CommRing R} →
    {L : Type u_2} →
      {inst_1 : RightPreLieRing L} →
        {P : Sort u} →
          {toModule : Module R L} →
            {toIsScalarTower : IsScalarTower R L L} →
              {toSMulCommClass : SMulCommClass R L L} →
                {toModule' : Module R L} →
                  {toIsScalarTower' : IsScalarTower R L L} →
                    {toSMulCommClass' : SMulCommClass R L L} →
                      { toModule := toModule, toIsScalarTower := toIsScalarTower, toSMulCommClass := toSMulCommClass } =
                          { toModule := toModule', toIsScalarTower := toIsScalarTower',
                            toSMulCommClass := toSMulCommClass' } →
                        (toModule ≍ toModule' → P) → P

Defined in

Mathlib.Algebra.NonAssoc.PreLie.Basic

Cited by

0 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms