Theorems · Theorem · group theory
SMulMemClass.smul_mem
∀ {S : Type u_1} {R : outParam (Type u_2)} {M : Type u_3} {inst : SMul R M} {inst_1 : SetLike S M}
[self : SMulMemClass S R M] {s : S} (r : R) {m : M}, m ∈ s → r • m ∈ sMultiplication by a scalar on an element of the set remains in the set.
- Cited by
- 55 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses no axioms
- Assumes
- SMulMemClass
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- SetLikestatement and proof · cited by 1,084
- SMulMemClassstatement and proof · cited by 77
Cited by55
Results whose statement or proof uses this declaration.
- algebraMap_memproof · cited by 23
- Subalgebra.smul_memproof · cited by 20
- LieSubalgebra.smul_memproof · cited by 6
- NonUnitalAlgebra.adjoin_inductionstatement and proof · cited by 4
- LieAlgebra.Basis.iSup_cartan_borelLower_borelUpper_eq_topproof · cited by 4
- LieAlgebra.IsKilling.chainTopCoeff_zero_rightproof · cited by 4
- LieAlgebra.IsKilling.sl2SubmoduleOfRoot_eq_supproof · cited by 3
- SMulMemClass.ofIsScalarTowerproof · cited by 3
- IsLinearTopology.mk_of_hasBasisproof · cited by 3
- Convexity.isConvexSet_coeproof · cited by 2
- AlgHomClass.unitization_injectiveproof · cited by 2
- Module.End.apply_eq_of_mem_of_comm_of_isFinitelySemisimple_of_isNilproof · cited by 2