Theorems · Definition · nonassociative algebras

LieAdmissibleRing.mk.noConfusion

{L : Type u_1} →
  {P : Sort u} →
    {toNonUnitalNonAssocRing : NonUnitalNonAssocRing L} →
      {assoc_def :
          ∀ (x y z : L),
            associator x y z + associator z x y + associator y z x =
              associator y x z + associator z y x + associator x z y} →
        {toNonUnitalNonAssocRing' : NonUnitalNonAssocRing L} →
          {assoc_def' :
              ∀ (x y z : L),
                associator x y z + associator z x y + associator y z x =
                  associator y x z + associator z y x + associator x z y} →
            { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing, assoc_def := assoc_def } =
                { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing', assoc_def := assoc_def' } →
              (toNonUnitalNonAssocRing ≍ toNonUnitalNonAssocRing' → P) → P

Defined in

Mathlib.Algebra.NonAssoc.LieAdmissible.Defs

Cited by

0 results in Mathlib

Foundations

Depth 12 from the axioms · uses no axioms