Theorems · Definition · commutative algebra

RingHom.fst

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

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

Defined in

Mathlib.Algebra.Ring.Prod

Cited by

36 results in Mathlib

Foundations

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

Assumes

NonAssocSemiringNonAssocSemiring