Theorems · Definition · nonassociative algebras
CentroidHom.comp
{α : Type u_5} → [inst : NonUnitalNonAssocSemiring α] → CentroidHom α → CentroidHom α → CentroidHom αComposition of CentroidHoms as a CentroidHom.
- Defined in
- Mathlib.Algebra.Ring.CentroidHom
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 15 from the axioms · uses propext, Quot.sound
- Assumes
- NonUnitalNonAssocSemiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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
- AddMonoidHom.compproof · cited by 339
- CentroidHomstatement and proof · cited by 67
- CentroidHom.toAddMonoidHomproof · cited by 4
Cited by8
Results whose statement or proof uses this declaration.
- CentroidHom.comp_applystatement · cited by 1
- CentroidHom.comp_assocstatement · cited by 0
- CentroidHom.comp_idstatement · cited by 0
- CentroidHom.cancel_leftstatement and proof · cited by 0
- CentroidHom.cancel_rightstatement and proof · cited by 0
- CentroidHom.id_compstatement · cited by 0
- CentroidHom.coe_compstatement · cited by 0
- CentroidHom.coe_comp_addMonoidHomstatement · cited by 0