Theorems · Definition · group theory

AddMonoid.casesOn

{M : Type u} →
  {motive : AddMonoid M → Sort u_1} →
    (t : AddMonoid M) →
      ([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 : ∀ (x : M), 0 • x = 0) →
                    (nsmul_succ : ∀ (n : ℕ) (x : M), (n + 1) • x = n • x + x) →
                      motive
                        { toAddSemigroup := toAddSemigroup, toZero := toZero, zero_add := zero_add,
                          add_zero := add_zero, toNSMul := toNSMul, nsmul_zero := nsmul_zero,
                          nsmul_succ := nsmul_succ }) →
        motive t

Defined in

Mathlib.Algebra.Group.Defs

Cited by

4 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms