Theorems · Definition · group theory
AddMonoidHom.snd
(M : Type u_3) → (N : Type u_4) → [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → M × N →+ N
Given additive monoids A, B, the natural projection homomorphism
from A × B to B
- Defined in
- Mathlib.Algebra.Group.Prod
- Cited by
- 42 results in Mathlib
- Foundations
- Depth 9 from the axioms · uses no axioms
- Assumes
- AddZeroClassAddZeroClass
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddMonoidHomstatement · cited by 3,230
- AddZeroClassstatement and proof · cited by 1,237
Cited by59
Results whose statement or proof uses this declaration.
- RingHom.sndproof · cited by 39
- AddMonoidHom.prodMapproof · cited by 15
- NonUnitalRingHom.sndproof · cited by 10
- AddSubgroup.goursatSndproof · cited by 8
- AddSubgroup.goursatFstproof · cited by 8
- AddMonoidHom.coprodproof · cited by 7
- AddCommGrpCat.binaryProductLimitConeproof · cited by 6
- Prod.snd_sumproof · cited by 5
- CategoryTheory.CommShift₂Setup.toTwistShiftDatastatement · cited by 4
- AddSubgroup.normal_goursatSndproof · cited by 3
- OrderAddMonoidHom.sndproof · cited by 3
- AddCommGrpCat.biprodIsoProd_inv_comp_descstatement · cited by 2