Theorems · Definition · commutative algebra

AddGroupWithOne.mk.noConfusion

{R : Type u} →
  {P : Sort u_1} →
    {toIntCast : IntCast R} →
      {toAddMonoidWithOne : AddMonoidWithOne R} →
        {toNeg : Neg R} →
          {toSub : Sub R} →
            {toZSMul : ZSMul R} →
              {sub_eq_add_neg : autoParam (∀ (a b : R), a - b = a + -b) SubNegMonoid.sub_eq_add_neg._autoParam} →
                {zsmul_zero' : autoParam (∀ (a : R), 0 • a = 0) SubNegMonoid.zsmul_zero'._autoParam} →
                  {zsmul_succ' :
                      autoParam (∀ (n : ℕ) (a : R), ↑n.succ • a = ↑n • a + a) SubNegMonoid.zsmul_succ'._autoParam} →
                    {zsmul_neg' :
                        autoParam (∀ (n : ℕ) (a : R), Int.negSucc n • a = -(↑n.succ • a))
                          SubNegMonoid.zsmul_neg'._autoParam} →
                      {neg_add_cancel : ∀ (a : R), -a + a = 0} →
                        {intCast_ofNat :
                            autoParam (∀ (n : ℕ), IntCast.intCast ↑n = ↑n) AddGroupWithOne.intCast_ofNat._autoParam} →
                          {intCast_negSucc :
                              autoParam (∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1))
                                AddGroupWithOne.intCast_negSucc._autoParam} →
                            {toIntCast' : IntCast R} →
                              {toAddMonoidWithOne' : AddMonoidWithOne R} →
                                {toNeg' : Neg R} →
                                  {toSub' : Sub R} →
                                    {toZSMul' : ZSMul R} →
                                      {sub_eq_add_neg' :
                                          autoParam (∀ (a b : R), a - b = a + -b)
                                            SubNegMonoid.sub_eq_add_neg._autoParam} →
                                        {zsmul_zero'' :
                                            autoParam (∀ (a : R), 0 • a = 0) SubNegMonoid.zsmul_zero'._autoParam} →
                                          {zsmul_succ'' :
                                              autoParam (∀ (n : ℕ) (a : R), ↑n.succ • a = ↑n • a + a)
                                                SubNegMonoid.zsmul_succ'._autoParam} →
                                            {zsmul_neg'' :
                                                autoParam (∀ (n : ℕ) (a : R), Int.negSucc n • a = -(↑n.succ • a))
                                                  SubNegMonoid.zsmul_neg'._autoParam} →
                                              {neg_add_cancel' : ∀ (a : R), -a + a = 0} →
                                                {intCast_ofNat' :
                                                    autoParam (∀ (n : ℕ), IntCast.intCast ↑n = ↑n)
                                                      AddGroupWithOne.intCast_ofNat._autoParam} →
                                                  {intCast_negSucc' :
                                                      autoParam (∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1))
                                                        AddGroupWithOne.intCast_negSucc._autoParam} →
                                                    { toIntCast := toIntCast, toAddMonoidWithOne := toAddMonoidWithOne,
                                                          toNeg := toNeg, toSub := toSub, toZSMul := toZSMul,
                                                          sub_eq_add_neg := sub_eq_add_neg, zsmul_zero' := zsmul_zero',
                                                          zsmul_succ' := zsmul_succ', zsmul_neg' := zsmul_neg',
                                                          neg_add_cancel := neg_add_cancel,
                                                          intCast_ofNat := intCast_ofNat,
                                                          intCast_negSucc := intCast_negSucc } =
                                                        { toIntCast := toIntCast',
                                                          toAddMonoidWithOne := toAddMonoidWithOne', toNeg := toNeg',
                                                          toSub := toSub', toZSMul := toZSMul',
                                                          sub_eq_add_neg := sub_eq_add_neg',
                                                          zsmul_zero' := zsmul_zero'', zsmul_succ' := zsmul_succ'',
                                                          zsmul_neg' := zsmul_neg'', neg_add_cancel := neg_add_cancel',
                                                          intCast_ofNat := intCast_ofNat',
                                                          intCast_negSucc := intCast_negSucc' } →
                                                      (toIntCast ≍ toIntCast' →
                                                          toAddMonoidWithOne ≍ toAddMonoidWithOne' →
                                                            toNeg ≍ toNeg' → toSub ≍ toSub' → toZSMul ≍ toZSMul' → P) →
                                                        P

Defined in

Mathlib.Data.Int.Cast.Defs

Cited by

1 results in Mathlib

Foundations

Depth 14 from the axioms · uses no axioms