Mathlib Map

Theorems · Definition · group theory

CommMonoid.casesOn

{M : Type u} →
  {motive : CommMonoid M → Sort u_1} →
    (t : CommMonoid M) →
      ([toMonoid : Monoid M] →
          (mul_comm : ∀ (a b : M), a * b = b * a) → motive { toMonoid := toMonoid, mul_comm := mul_comm }) →
        motive t
Defined in
Mathlib.Algebra.Group.Defs
Cited by
2 results in Mathlib
Foundations
Depth 6 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

CancelCommMonoid.toCommMonoid_injective · cited by 1CancelCommMonoid.toCommMo…CommMonoid.toMonoid_injective · cited by 1CommMonoid.toMonoid_injec…CommMonoid.noConfusion · cited by 0CommMonoid.noConfusionCommMonoid.noConfusionType · cited by 0CommMonoid.noConfusionTypeMonoid · cited by 3887MonoidCommMonoid · cited by 2264CommMonoidCommMonoid.casesOnCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Monoidstatement and proof · cited by 3,887
  • CommMonoidstatement and proof · cited by 2,264

Cited by4

Results whose statement or proof uses this declaration.