Theorems · Definition · ring theory

NonUnitalSubringClass.recOn

{S : Type u_1} →
  {R : Type u} →
    [inst : NonUnitalNonAssocRing R] →
      [inst_1 : SetLike S R] →
        {motive : NonUnitalSubringClass S R → Sort u_2} →
          (t : NonUnitalSubringClass S R) →
            ([toNonUnitalSubsemiringClass : NonUnitalSubsemiringClass S R] →
                [toNegMemClass : NegMemClass S R] → motive ⋯) →
              motive t

Defined in

Mathlib.RingTheory.NonUnitalSubring.Defs

Cited by

0 results in Mathlib

Foundations

Depth 15 from the axioms · uses propext

Assumes

NonUnitalNonAssocRingSetLike