Theorems · Definition · ring theory

NonAssocRing.casesOn

{α : Type u_1} →
  {motive : NonAssocRing α → Sort u} →
    (t : NonAssocRing α) →
      ([toNonUnitalNonAssocRing : NonUnitalNonAssocRing α] →
          [toOne : One α] →
            (one_mul : ∀ (a : α), 1 * a = a) →
              (mul_one : ∀ (a : α), a * 1 = a) →
                [toNatCast : NatCast α] →
                  (natCast_zero : ↑0 = 0) →
                    (natCast_succ : ∀ (n : ℕ), ↑(n + 1) = ↑n + 1) →
                      [toIntCast : IntCast α] →
                        (intCast_ofNat : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n) →
                          (intCast_negSucc : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)) →
                            motive
                              { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing, toOne := toOne, one_mul := one_mul,
                                mul_one := mul_one, toNatCast := toNatCast, natCast_zero := natCast_zero,
                                natCast_succ := natCast_succ, toIntCast := toIntCast, intCast_ofNat := intCast_ofNat,
                                intCast_negSucc := intCast_negSucc }) →
        motive t

Defined in

Mathlib.Algebra.Ring.Defs

Cited by

1 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms