Theorems · Definition · ring theory

NonUnitalSubsemiringClass.subtype

{R : Type u} →
  {S : Type v} →
    [inst : NonUnitalNonAssocSemiring R] →
      [inst_1 : SetLike S R] → [inst_2 : NonUnitalSubsemiringClass S R] → (s : S) → ↥s →ₙ+* R

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

Defined in

Mathlib.RingTheory.NonUnitalSubsemiring.Defs

Cited by

5 results in Mathlib

Foundations

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

Assumes

NonUnitalNonAssocSemiringSetLikeNonUnitalSubsemiringClass