Theorems · Definition · group theory
MonoidWithZeroHom.comp
{α : Type u_2} →
{β : Type u_3} →
{γ : Type u_4} →
[inst : MulZeroOneClass α] →
[inst_1 : MulZeroOneClass β] → [inst_2 : MulZeroOneClass γ] → (β →*₀ γ) → (α →*₀ β) → α →*₀ γComposition of MonoidWithZeroHoms as a MonoidWithZeroHom.
- Defined in
- Mathlib.Algebra.GroupWithZero.Hom
- Cited by
- 34 results in Mathlib
- Foundations
- Depth 13 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- MonoidWithZeroHomstatement and proof · cited by 704
- MulZeroOneClassstatement and proof · cited by 184
Cited by48
Results whose statement or proof uses this declaration.
- Cardinal.toNatproof · cited by 153
- MonoidWithZeroHom.ValueGroup₀.embeddingproof · cited by 47
- Valuation.comapproof · cited by 15
- OrderMonoidWithZeroHom.compproof · cited by 14
- MonoidWithZeroHom.inlproof · cited by 13
- MonoidWithZeroHom.inrproof · cited by 12
- ValuativeExtension.mapValueGroupWithZeroproof · cited by 5
- Valuation.mapproof · cited by 4
- LinearOrderedCommGroupWithZero.inlproof · cited by 4
- LinearOrderedCommGroupWithZero.inrproof · cited by 3
- ENNReal.toRealHomproof · cited by 3
- MonoidWithZeroHom.comp_applystatement · cited by 3