Theorems · Theorem · ring theory
LinearMap.comp_smul
∀ {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} {M₃ : Type u_11} [inst : Semiring R]
[inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M]
[inst_5 : Monoid S] [inst_6 : DistribMulAction S M₂] [inst_7 : Module R M₂] [inst_8 : Module R M₃]
[inst_9 : SMulCommClass R S M₂] [inst_10 : DistribMulAction S M₃] [inst_11 : SMulCommClass R S M₃]
[LinearMap.CompatibleSMul M₃ M₂ S R] (g : M₃ →ₗ[R] M₂) (a : S) (f : M →ₗ[R] M₃), g ∘ₗ (a • f) = a • g ∘ₗ f- Defined in
- Mathlib.Algebra.Module.LinearMap.Defs
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 25 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Modulestatement and proof · cited by 20,661
- RingHom.idstatement and proof · cited by 18,349
- Semiringstatement and proof · cited by 13,802
- AddCommMonoidstatement and proof · cited by 12,281
- LinearMapstatement and proof · cited by 10,215
- Monoidstatement and proof · cited by 3,887
- SMulCommClassstatement and proof · cited by 1,927
- LinearMap.compstatement · cited by 1,642
- LinearMap.extproof · cited by 844
- DistribMulActionstatement and proof · cited by 584
- LinearMap.CompatibleSMulstatement and proof · cited by 86
Cited by3
Results whose statement or proof uses this declaration.
- Module.FinitePresentation.exists_lift_of_isLocalizedModuleproof · cited by 3
- exists_bijective_map_powersproof · cited by 3
- LieModule.traceForm_genWeightSpace_eqproof · cited by 1