Theorems · Definition · nonassociative algebras

LieRinehartSubalgebra.noConfusion

{P : Sort u} →
  {A : Type u_1} →
    {L : Type u_2} →
      {inst : CommRing A} →
        {inst_1 : LieRing L} →
          {inst_2 : Module A L} →
            {t : LieRinehartSubalgebra A L} →
              {A' : Type u_1} →
                {L' : Type u_2} →
                  {inst' : CommRing A'} →
                    {inst'_1 : LieRing L'} →
                      {inst'_2 : Module A' L'} →
                        {t' : LieRinehartSubalgebra A' L'} →
                          A = A' →
                            L = L' →
                              inst ≍ inst' →
                                inst_1 ≍ inst'_1 →
                                  inst_2 ≍ inst'_2 → t ≍ t' → LieRinehartSubalgebra.noConfusionType P t t'

Defined in

Mathlib.Algebra.LieRinehartAlgebra.Subalgebra

Cited by

0 results in Mathlib

Foundations

Depth 12 from the axioms · uses no axioms