Theorems · Theorem · group theory
map_smul
∀ {F : Type u_8} {M : Type u_9} {X : Type u_10} {Y : Type u_11} [inst : SMul M X] [inst_1 : SMul M Y]
[inst_2 : FunLike F X Y] [MulActionHomClass F M X Y] (f : F) (c : M) (x : X), f (c • x) = c • f x- Defined in
- Mathlib.GroupTheory.GroupAction.Hom
- Cited by
- 566 results in Mathlib
- Foundations
- Depth 5 from the axioms, rests on 13 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- FunLikestatement and proof · cited by 2,560
- MulActionSemiHomClass.map_smulₛₗproof · cited by 49
- MulActionHomClassstatement and proof · cited by 16
Cited by566
Results whose statement or proof uses this declaration.
- LinearMap.map_smulproof · cited by 60
- Module.Free.of_equivproof · cited by 23
- IsBaseChange.of_equivproof · cited by 17
- LinearIsometry.inner_map_mapproof · cited by 16
- AffineMap.apply_lineMapproof · cited by 16
- Module.projective_lifting_propertyproof · cited by 13
- LieAlgebra.IsKilling.root_apply_corootproof · cited by 11
- MeasureTheory.L1.setToL1_eq_setToL1SCLMproof · cited by 11
- Orientation.oangle_smul_right_of_posproof · cited by 10
- Module.Projective.of_equivproof · cited by 9
- Orientation.oangle_smul_left_of_posproof · cited by 8
- AddMonoidAlgebra.scalarTensorEquiv_tmulproof · cited by 8
Showing the 200 most cited of 566.