Theorems · Definition · commutative algebra
smulAddHom
(R : Type u_1) → (M : Type u_3) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → R →+ M →+ M
A convenience alias for Module.toAddMonoidEnd as an AddMonoidHom, usually to allow the
use of AddMonoidHom.flip.
- Defined in
- Mathlib.Algebra.Module.End
- Cited by
- 17 results in Mathlib
- Foundations
- Depth 28 from the axioms · uses propext, Quot.sound
- Assumes
- SemiringAddCommMonoidModule
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Modulestatement and proof · cited by 20,661
- Semiringstatement and proof · cited by 13,802
- AddCommMonoidstatement and proof · cited by 12,281
- AddMonoidHomstatement · cited by 3,230
- RingHom.toAddMonoidHomproof · cited by 17
- Module.toAddMonoidEndproof · cited by 1
Cited by21
Results whose statement or proof uses this declaration.
- Finset.sum_smulproof · cited by 30
- Finsupp.toFreeAbelianGroupproof · cited by 8
- HasSum.smul_constproof · cited by 6
- IsAddUnit.smul_rightproof · cited by 3
- Finsupp.toFreeAbelianGroup_singleproof · cited by 3
- AddMonoidAlgebra.liftMagmaproof · cited by 2
- MonoidAlgebra.liftMagmaproof · cited by 2
- smulAddHom_applystatement · cited by 1
- Finsupp.toFreeAbelianGroup_comp_toFinsuppproof · cited by 1
- Module.IsTorsionBySet.hasSMulproof · cited by 1
- AddMonoidAlgebra.liftMagma_apply_applystatement · cited by 0
- Multiset.sum_smulproof · cited by 0