Theorems · Theorem · ring theory
Module.End.mul_apply
∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
(f g : Module.End R M) (x : M), (f * g) x = f (g x)- Defined in
- Mathlib.Algebra.Module.LinearMap.End
- Cited by
- 23 results in Mathlib
- Foundations
- Depth 25 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.
- DFunLike.coestatement · cited by 62,936
- Modulestatement and proof · cited by 20,661
- RingHom.idstatement · cited by 18,349
- Semiringstatement and proof · cited by 13,802
- AddCommMonoidstatement and proof · cited by 12,281
- Module.Endstatement and proof · cited by 774
Cited by23
Results whose statement or proof uses this declaration.
- Module.End.pow_map_zero_of_leproof · cited by 6
- fwdDiff_iter_eq_sum_shiftproof · cited by 5
- IsSl2Triple.HasPrimitiveVectorWith.lie_h_pow_toEnd_fproof · cited by 3
- IsSl2Triple.HasPrimitiveVectorWith.lie_e_pow_succ_toEnd_fproof · cited by 3
- Module.End.aeval_apply_of_hasEigenvectorproof · cited by 2
- LinearMap.IsIdempotentElem.isPositive_iff_isSymmetricproof · cited by 2
- LinearMap.finrank_maxGenEigenspace_zero_eqproof · cited by 2
- LinearMap.IsSymmetric.mul_of_commuteproof · cited by 1
- LieModule.weight_vector_multiplicationproof · cited by 1
- IsSl2Triple.lie_h_pow_toEnd_eproof · cited by 1
- Module.End.genEigenspace_inf_le_addproof · cited by 1
- Module.End.genEigenspace_mem_invtSubmoduleproof · cited by 1