Theorems · Definition · ring theory

NonAssocRing.mk.noConfusion

{α : Type u_1} →
  {P : Sort u} →
    {toNonUnitalNonAssocRing : NonUnitalNonAssocRing α} →
      {toOne : One α} →
        {one_mul : ∀ (a : α), 1 * a = a} →
          {mul_one : ∀ (a : α), a * 1 = a} →
            {toNatCast : NatCast α} →
              {natCast_zero : autoParam (↑0 = 0) AddMonoidWithOne.natCast_zero._autoParam} →
                {natCast_succ : autoParam (∀ (n : ℕ), ↑(n + 1) = ↑n + 1) AddMonoidWithOne.natCast_succ._autoParam} →
                  {toIntCast : IntCast α} →
                    {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} →
                        {toNonUnitalNonAssocRing' : NonUnitalNonAssocRing α} →
                          {toOne' : One α} →
                            {one_mul' : ∀ (a : α), 1 * a = a} →
                              {mul_one' : ∀ (a : α), a * 1 = a} →
                                {toNatCast' : NatCast α} →
                                  {natCast_zero' : autoParam (↑0 = 0) AddMonoidWithOne.natCast_zero._autoParam} →
                                    {natCast_succ' :
                                        autoParam (∀ (n : ℕ), ↑(n + 1) = ↑n + 1)
                                          AddMonoidWithOne.natCast_succ._autoParam} →
                                      {toIntCast' : IntCast α} →
                                        {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} →
                                            { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing, toOne := toOne,
                                                  one_mul := one_mul, mul_one := mul_one, toNatCast := toNatCast,
                                                  natCast_zero := natCast_zero, natCast_succ := natCast_succ,
                                                  toIntCast := toIntCast, intCast_ofNat := intCast_ofNat,
                                                  intCast_negSucc := intCast_negSucc } =
                                                { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing', toOne := toOne',
                                                  one_mul := one_mul', mul_one := mul_one', toNatCast := toNatCast',
                                                  natCast_zero := natCast_zero', natCast_succ := natCast_succ',
                                                  toIntCast := toIntCast', intCast_ofNat := intCast_ofNat',
                                                  intCast_negSucc := intCast_negSucc' } →
                                              (toNonUnitalNonAssocRing ≍ toNonUnitalNonAssocRing' →
                                                  toOne ≍ toOne' →
                                                    toNatCast ≍ toNatCast' → toIntCast ≍ toIntCast' → P) →
                                                P

Defined in

Mathlib.Algebra.Ring.Defs

Cited by

1 results in Mathlib

Foundations

Depth 14 from the axioms · uses no axioms