Theorems · Definition · commutative algebra

AddMonoidWithOne.casesOn

{R : Type u_2} →
  {motive : AddMonoidWithOne R → Sort u} →
    (t : AddMonoidWithOne R) →
      ([toNatCast : NatCast R] →
          [toAddMonoid : AddMonoid R] →
            [toOne : One R] →
              (natCast_zero : ↑0 = 0) →
                (natCast_succ : ∀ (n : ℕ), ↑(n + 1) = ↑n + 1) →
                  motive
                    { toNatCast := toNatCast, toAddMonoid := toAddMonoid, toOne := toOne, natCast_zero := natCast_zero,
                      natCast_succ := natCast_succ }) →
        motive t

Defined in

Mathlib.Data.Nat.Cast.Defs

Cited by

1 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms