Theorems · Definition · logic and foundations

FirstOrder.Ring.CompatibleRing.mk.noConfusion

{R : Type u_2} →
  {inst : Add R} →
    {inst_1 : Mul R} →
      {inst_2 : Neg R} →
        {inst_3 : One R} →
          {inst_4 : Zero R} →
            {P : Sort u} →
              {toStructure : FirstOrder.Language.ring.Structure R} →
                {funMap_add :
                    ∀ (x : Fin 2 → R), FirstOrder.Language.Structure.funMap FirstOrder.Ring.addFunc x = x 0 + x 1} →
                  {funMap_mul :
                      ∀ (x : Fin 2 → R), FirstOrder.Language.Structure.funMap FirstOrder.Ring.mulFunc x = x 0 * x 1} →
                    {funMap_neg :
                        ∀ (x : Fin 1 → R), FirstOrder.Language.Structure.funMap FirstOrder.Ring.negFunc x = -x 0} →
                      {funMap_zero :
                          ∀ (x : Fin 0 → R), FirstOrder.Language.Structure.funMap FirstOrder.Ring.zeroFunc x = 0} →
                        {funMap_one :
                            ∀ (x : Fin 0 → R), FirstOrder.Language.Structure.funMap FirstOrder.Ring.oneFunc x = 1} →
                          {toStructure' : FirstOrder.Language.ring.Structure R} →
                            {funMap_add' :
                                ∀ (x : Fin 2 → R),
                                  FirstOrder.Language.Structure.funMap FirstOrder.Ring.addFunc x = x 0 + x 1} →
                              {funMap_mul' :
                                  ∀ (x : Fin 2 → R),
                                    FirstOrder.Language.Structure.funMap FirstOrder.Ring.mulFunc x = x 0 * x 1} →
                                {funMap_neg' :
                                    ∀ (x : Fin 1 → R),
                                      FirstOrder.Language.Structure.funMap FirstOrder.Ring.negFunc x = -x 0} →
                                  {funMap_zero' :
                                      ∀ (x : Fin 0 → R),
                                        FirstOrder.Language.Structure.funMap FirstOrder.Ring.zeroFunc x = 0} →
                                    {funMap_one' :
                                        ∀ (x : Fin 0 → R),
                                          FirstOrder.Language.Structure.funMap FirstOrder.Ring.oneFunc x = 1} →
                                      { toStructure := toStructure, funMap_add := funMap_add, funMap_mul := funMap_mul,
                                            funMap_neg := funMap_neg, funMap_zero := funMap_zero,
                                            funMap_one := funMap_one } =
                                          { toStructure := toStructure', funMap_add := funMap_add',
                                            funMap_mul := funMap_mul', funMap_neg := funMap_neg',
                                            funMap_zero := funMap_zero', funMap_one := funMap_one' } →
                                        (toStructure ≍ toStructure' → P) → P

Defined in

Mathlib.ModelTheory.Algebra.Ring.Basic

Cited by

0 results in Mathlib

Foundations

Depth 30 from the axioms · uses propext