Theorems · Definition · group theory

Monoid.mk.noConfusion

{M : Type u} →
  {P : Sort u_1} →
    {toSemigroup : Semigroup M} →
      {toOne : One M} →
        {one_mul : ∀ (a : M), 1 * a = a} →
          {mul_one : ∀ (a : M), a * 1 = a} →
            {toNPow : NPow M} →
              {npow_zero : autoParam (∀ (x : M), x ^ 0 = 1) Monoid.npow_zero._autoParam} →
                {npow_succ : autoParam (∀ (n : ℕ) (x : M), x ^ (n + 1) = x ^ n * x) Monoid.npow_succ._autoParam} →
                  {toSemigroup' : Semigroup M} →
                    {toOne' : One M} →
                      {one_mul' : ∀ (a : M), 1 * a = a} →
                        {mul_one' : ∀ (a : M), a * 1 = a} →
                          {toNPow' : NPow M} →
                            {npow_zero' : autoParam (∀ (x : M), x ^ 0 = 1) Monoid.npow_zero._autoParam} →
                              {npow_succ' :
                                  autoParam (∀ (n : ℕ) (x : M), x ^ (n + 1) = x ^ n * x) Monoid.npow_succ._autoParam} →
                                { toSemigroup := toSemigroup, toOne := toOne, one_mul := one_mul, mul_one := mul_one,
                                      toNPow := toNPow, npow_zero := npow_zero, npow_succ := npow_succ } =
                                    { toSemigroup := toSemigroup', toOne := toOne', one_mul := one_mul',
                                      mul_one := mul_one', toNPow := toNPow', npow_zero := npow_zero',
                                      npow_succ := npow_succ' } →
                                  (toSemigroup ≍ toSemigroup' → toOne ≍ toOne' → toNPow ≍ toNPow' → P) → P

Defined in

Mathlib.Algebra.Group.Defs

Cited by

2 results in Mathlib

Foundations

Depth 14 from the axioms · uses no axioms