Theorems · Definition · commutative algebra
NonUnitalRingHom.snd
(R : Type u_1) → (S : Type u_3) → [inst : NonUnitalNonAssocSemiring R] → [inst_1 : NonUnitalNonAssocSemiring S] → R × S →ₙ+* S
Given non-unital semirings R, S, the natural projection homomorphism from R × S to S.
- Defined in
- Mathlib.Algebra.Ring.Prod
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 16 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddMonoidHomproof · cited by 3,230
- NonUnitalNonAssocSemiringstatement and proof · cited by 1,081
- MulHomproof · cited by 299
- NonUnitalRingHomstatement · cited by 157
- AddMonoidHom.sndproof · cited by 42
- MulHom.sndproof · cited by 9
Cited by11
Results whose statement or proof uses this declaration.
- NonUnitalRingHom.prodMapproof · cited by 3
- NonUnitalSubsemiring.range_sndstatement and proof · cited by 1
- NonUnitalSubring.top_prodstatement · cited by 1
- NonUnitalSubsemiring.top_prodstatement · cited by 1
- NonUnitalRingHom.prod_uniquestatement · cited by 0
- NonUnitalRingHom.snd_comp_prodstatement · cited by 0
- NonUnitalSubring.range_sndstatement · cited by 0
- NonUnitalSubring.top_prod_topproof · cited by 0
- NonUnitalRingHom.coe_sndstatement · cited by 0
- NonUnitalSubsemiring.top_prod_topproof · cited by 0
- NonUnitalRingHom.prodMap_defstatement · cited by 0