Theorems · Definition · ring theory
AddMonoidHom.mul
{R : Type u_1} → [inst : NonUnitalNonAssocSemiring R] → R →+ R →+ RMultiplication of an element of a (semi)ring is an AddMonoidHom in both arguments.
This is a more-strongly bundled version of AddMonoidHom.mulLeft and AddMonoidHom.mulRight.
Stronger versions of this exists for algebras as LinearMap.mul, NonUnitalAlgHom.mul
and Algebra.lmul.
- Defined in
- Mathlib.Algebra.Ring.Basic
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 21 from the axioms · uses propext, Quot.sound
- Assumes
- NonUnitalNonAssocSemiring
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.
- AddMonoidHomstatement · cited by 3,230
- NonUnitalNonAssocSemiringstatement and proof · cited by 1,081
- AddMonoidHom.mulLeftproof · cited by 23
Cited by12
Results whose statement or proof uses this declaration.
- AddSubmonoid.mulproof · cited by 18
- AddMonoid.End.mulLeftproof · cited by 11
- AddMonoid.End.mulRightproof · cited by 9
- AddMonoidHom.mulRight₃proof · cited by 3
- AddMonoidHom.mulLeft₃proof · cited by 3
- AddMonoidAlgebra.toDirectSum_mulproof · cited by 1
- AddMonoidHom.map_mul_iffstatement · cited by 1
- AddMonoidHom.coe_flip_mulstatement · cited by 0
- Polynomial.hasseDeriv_mulproof · cited by 0
- AddMonoidHom.coe_mulstatement · cited by 0
- AddMonoidHom.mul_applystatement · cited by 0
- Set.mem_center_iff_addMonoidHomstatement and proof · cited by 0