Theorems · Definition · group theory

AddMonoid.mk.noConfusion

{M : Type u} →
  {P : Sort u_1} →
    {toAddSemigroup : AddSemigroup M} →
      {toZero : Zero M} →
        {zero_add : ∀ (a : M), 0 + a = a} →
          {add_zero : ∀ (a : M), a + 0 = a} →
            {toNSMul : NSMul M} →
              {nsmul_zero : autoParam (∀ (x : M), 0 • x = 0) AddMonoid.nsmul_zero._autoParam} →
                {nsmul_succ : autoParam (∀ (n : ℕ) (x : M), (n + 1) • x = n • x + x) AddMonoid.nsmul_succ._autoParam} →
                  {toAddSemigroup' : AddSemigroup M} →
                    {toZero' : Zero M} →
                      {zero_add' : ∀ (a : M), 0 + a = a} →
                        {add_zero' : ∀ (a : M), a + 0 = a} →
                          {toNSMul' : NSMul M} →
                            {nsmul_zero' : autoParam (∀ (x : M), 0 • x = 0) AddMonoid.nsmul_zero._autoParam} →
                              {nsmul_succ' :
                                  autoParam (∀ (n : ℕ) (x : M), (n + 1) • x = n • x + x)
                                    AddMonoid.nsmul_succ._autoParam} →
                                { toAddSemigroup := toAddSemigroup, toZero := toZero, zero_add := zero_add,
                                      add_zero := add_zero, toNSMul := toNSMul, nsmul_zero := nsmul_zero,
                                      nsmul_succ := nsmul_succ } =
                                    { toAddSemigroup := toAddSemigroup', toZero := toZero', zero_add := zero_add',
                                      add_zero := add_zero', toNSMul := toNSMul', nsmul_zero := nsmul_zero',
                                      nsmul_succ := nsmul_succ' } →
                                  (toAddSemigroup ≍ toAddSemigroup' → toZero ≍ toZero' → toNSMul ≍ toNSMul' → P) → P

Defined in

Mathlib.Algebra.Group.Defs

Cited by

2 results in Mathlib

Foundations

Depth 14 from the axioms · uses no axioms