Theorems · Definition · logic and foundations

FirstOrder.Ring.CompatibleRing.casesOn

{R : Type u_2} →
  [inst : Add R] →
    [inst_1 : Mul R] →
      [inst_2 : Neg R] →
        [inst_3 : One R] →
          [inst_4 : Zero R] →
            {motive : FirstOrder.Ring.CompatibleRing R → Sort u} →
              (t : FirstOrder.Ring.CompatibleRing R) →
                ([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) →
                              motive
                                { toStructure := toStructure, funMap_add := funMap_add, funMap_mul := funMap_mul,
                                  funMap_neg := funMap_neg, funMap_zero := funMap_zero, funMap_one := funMap_one }) →
                  motive t

Defined in

Mathlib.ModelTheory.Algebra.Ring.Basic

Cited by

0 results in Mathlib

Foundations

Depth 27 from the axioms · uses propext

Assumes

AddMulNegOneZero