Theorems · Definition · group theory

Monoid.recOn

{M : Type u} →
  {motive : Monoid M → Sort u_1} →
    (t : Monoid M) →
      ([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 : ∀ (x : M), x ^ 0 = 1) →
                    (npow_succ : ∀ (n : ℕ) (x : M), x ^ (n + 1) = x ^ n * x) →
                      motive
                        { toSemigroup := toSemigroup, toOne := toOne, one_mul := one_mul, mul_one := mul_one,
                          toNPow := toNPow, npow_zero := npow_zero, npow_succ := npow_succ }) →
        motive t

Defined in

Mathlib.Algebra.Group.Defs

Cited by

0 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms