Theorems · Definition · ring theory

Semiring.casesOn

{α : Type u} →
  {motive : Semiring α → Sort u_1} →
    (t : Semiring α) →
      ([toAddCommMonoid : AddCommMonoid α] →
          [toMonoid : Monoid α] →
            (zero_mul : ∀ (a : α), 0 * a = 0) →
              (mul_zero : ∀ (a : α), a * 0 = 0) →
                (left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c) →
                  (right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c) →
                    [toNatCast : NatCast α] →
                      (natCast_zero : ↑0 = 0) →
                        (natCast_succ : ∀ (n : ℕ), ↑(n + 1) = ↑n + 1) →
                          motive
                            { toAddCommMonoid := toAddCommMonoid, toMonoid := toMonoid, zero_mul := zero_mul,
                              mul_zero := mul_zero, left_distrib := left_distrib, right_distrib := right_distrib,
                              toNatCast := toNatCast, natCast_zero := natCast_zero, natCast_succ := natCast_succ }) →
        motive t

Defined in

Mathlib.Algebra.Ring.Defs

Cited by

1 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms