Theorems · Definition · logic and foundations

FirstOrder.Ring.CompatibleRing.noConfusion

{P : Sort u} →
  {R : Type u_2} →
    {inst : Add R} →
      {inst_1 : Mul R} →
        {inst_2 : Neg R} →
          {inst_3 : One R} →
            {inst_4 : Zero R} →
              {t : FirstOrder.Ring.CompatibleRing R} →
                {R' : Type u_2} →
                  {inst' : Add R'} →
                    {inst'_1 : Mul R'} →
                      {inst'_2 : Neg R'} →
                        {inst'_3 : One R'} →
                          {inst'_4 : Zero R'} →
                            {t' : FirstOrder.Ring.CompatibleRing R'} →
                              R = R' →
                                inst ≍ inst' →
                                  inst_1 ≍ inst'_1 →
                                    inst_2 ≍ inst'_2 →
                                      inst_3 ≍ inst'_3 →
                                        inst_4 ≍ inst'_4 →
                                          t ≍ t' → FirstOrder.Ring.CompatibleRing.noConfusionType P t t'

Defined in

Mathlib.ModelTheory.Algebra.Ring.Basic

Cited by

0 results in Mathlib

Foundations

Depth 29 from the axioms · uses propext