Mathlib Map

Theorems · Definition · ring theory

AddMonoidHom.mulLeft

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

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

Defined in
Mathlib.Algebra.Ring.Basic
Cited by
23 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.mul_sum · cited by 196Finset.mul_sumLinearMap.mulLeft · cited by 34LinearMap.mulLeftAddChar.mulShift · cited by 26AddChar.mulShiftHasSum.mul_left · cited by 25HasSum.mul_leftAddMonoidHom.mul · cited by 7AddMonoidHom.mulAddChar.zmod · cited by 7AddChar.zmodPolynomial.derivative_prod · cited by 3Polynomial.derivative_prodAddMonoidHom.mulLeft₃ · cited by 3AddMonoidHom.mulLeft₃AddMonoidHom.mulRight₃ · cited by 3AddMonoidHom.mulRight₃mulLeft_continuous · cited by 2mulLeft_continuousMonoidAlgebra.single_commute · cited by 2MonoidAlgebra.single_comm…AddMonoidAlgebra.single_commute · cited by 2AddMonoidAlgebra.single_c…List.sum_map_mul_left · cited by 2List.sum_map_mul_leftTwoSidedIdeal.mem_span_iff_mem_addSubgroup_closure_absorbing · cited by 2TwoSidedIdeal.mem_span_if…mul_finsum' · cited by 1mul_finsum'AddMonoidHom · cited by 3230AddMonoidHomNonUnitalNonAssocSemiring · cited by 1081NonUnitalNonAssocSemiringAddMonoidHom.mulLeftCITED BYCITES

Cites2

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

Cited by29

Results whose statement or proof uses this declaration.