Theorems · Definition · commutative algebra

RingHom.snd

(R : Type u_1) → (S : Type u_3) → [inst : NonAssocSemiring R] → [inst_1 : NonAssocSemiring S] → R × S →+* S

Given semirings R, S, the natural projection homomorphism from R × S to S.

Defined in

Mathlib.Algebra.Ring.Prod

Cited by

39 results in Mathlib

Foundations

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

Assumes

NonAssocSemiringNonAssocSemiring