Mathlib Map

Theorems · Definition · ring theory

AddMonoidHom.mulRight

{R : Type u_1} → [inst : NonUnitalNonAssocSemiring R] → R → R →+ R

Right multiplication by an element of a (semi)ring is an AddMonoidHom

Defined in
Mathlib.Algebra.Ring.Basic
Cited by
20 results in Mathlib
Foundations
Depth 8 from the axioms · uses no axioms
Assumes
NonUnitalNonAssocSemiring
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Finset.sum_mul · cited by 112Finset.sum_mulLinearMap.mulRight · cited by 24LinearMap.mulRightHasSum.mul_right · cited by 11HasSum.mul_rightAddMonoidAlgebra.liftNC · cited by 7AddMonoidAlgebra.liftNCSkewMonoidAlgebra.liftNC · cited by 6SkewMonoidAlgebra.liftNCMonoidAlgebra.liftNC · cited by 6MonoidAlgebra.liftNCMonoidAlgebra.liftNC_single · cited by 6MonoidAlgebra.liftNC_sing…SkewMonoidAlgebra.liftNC_single · cited by 5SkewMonoidAlgebra.liftNC_…AddMonoidAlgebra.liftNC_single · cited by 4AddMonoidAlgebra.liftNC_s…TwoSidedIdeal.mem_span_iff_mem_addSubgroup_closure_absorbing · cited by 2TwoSidedIdeal.mem_span_if…MonoidAlgebra.single_commute · cited by 2MonoidAlgebra.single_comm…AddMonoidAlgebra.single_commute · cited by 2AddMonoidAlgebra.single_c…finsum_mul' · cited by 1finsum_mul'AddMonoidHom.mulLeft_eq_mulRight_iff_forall_commute · cited by 1AddMonoidHom.mulLeft_eq_m…AddMonoidHom.mulRight_apply · cited by 1AddMonoidHom.mulRight_app…AddMonoidHom · cited by 3230AddMonoidHomNonUnitalNonAssocSemiring · cited by 1081NonUnitalNonAssocSemiringAddMonoidHom.mulRightCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by24

Results whose statement or proof uses this declaration.