Theorems · Definition · ring theory

NonUnitalSubringClass.subtype

{R : Type u} →
  {S : Type v} →
    [inst : NonUnitalNonAssocRing R] → [inst_1 : SetLike S R] → [hSR : NonUnitalSubringClass S R] → (s : S) → ↥s →ₙ+* R

The natural non-unital ring hom from a non-unital subring of a non-unital ring R to R.

Defined in

Mathlib.RingTheory.NonUnitalSubring.Defs

Cited by

6 results in Mathlib

Foundations

Depth 24 from the axioms · uses propext, Quot.sound

Assumes

NonUnitalNonAssocRingSetLikeNonUnitalSubringClass