Theorems · Definition · commutative algebra
NonUnitalRingHom.fst
(R : Type u_1) → (S : Type u_3) → [inst : NonUnitalNonAssocSemiring R] → [inst_1 : NonUnitalNonAssocSemiring S] → R × S →ₙ+* R
Given non-unital semirings R, S, the natural projection homomorphism from R × S to R.
- Defined in
- Mathlib.Algebra.Ring.Prod
- Cited by
- 8 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.fstproof · cited by 39
- MulHom.fstproof · cited by 8
Cited by9
Results whose statement or proof uses this declaration.
- NonUnitalRingHom.prodMapproof · cited by 3
- NonUnitalSubsemiring.range_fststatement and proof · cited by 1
- NonUnitalRingHom.prod_uniquestatement · cited by 0
- NonUnitalRingHom.coe_fststatement · cited by 0
- NonUnitalSubring.prod_topstatement · cited by 0
- NonUnitalSubring.range_fststatement · cited by 0
- NonUnitalRingHom.fst_comp_prodstatement · cited by 0
- NonUnitalRingHom.prodMap_defstatement · cited by 0
- NonUnitalSubsemiring.prod_topstatement · cited by 0