Theorems · Theorem · group theory
smul_sub
∀ {M : Type u_1} {A : Type u_7} [inst : AddGroup A] [inst_1 : DistribSMul M A] (r : M) (x y : A),
r • (x - y) = r • x - r • y- Cited by
- 142 results in Mathlib
- Foundations
- Depth 13 from the axioms, rests on 64 definitions · uses propext
- Assumes
- AddGroupDistribSMul
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddGroupstatement and proof · cited by 4,410
- sub_eq_add_negproof · cited by 1,023
- smul_addproof · cited by 263
- smul_negproof · cited by 181
- DistribSMulstatement and proof · cited by 117
Cited by142
Results whose statement or proof uses this declaration.
- AffineMap.lineMap_apply_moduleproof · cited by 16
- dist_smul₀proof · cited by 11
- intervalIntegral.integral_smulproof · cited by 10
- Module.End.disjoint_genEigenspaceproof · cited by 7
- AffineSubspace.wSameSide_iff_exists_leftproof · cited by 5
- AnalyticAt.meromorphicTrailingCoeffAt_of_eq_nhdsNEproof · cited by 4
- circleIntegral.integral_subproof · cited by 4
- HasFDerivWithinAt.limproof · cited by 4
- isSMulRegular_iff_right_eq_zero_of_smulproof · cited by 4
- EuclideanGeometry.inner_pos_or_eq_of_dist_le_radiusproof · cited by 3
- Real.circleAverage_subproof · cited by 3
- segment_eq_image'proof · cited by 3