Theorems · Definition · commutative algebra

SubsemiringClass.subtype

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

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

Defined in

Mathlib.Algebra.Ring.Subsemiring.Defs

Cited by

5 results in Mathlib

Foundations

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

Assumes

NonAssocSemiringSetLikeSubsemiringClass