Theorems · Theorem · commutative algebra
sub_smul
∀ {R : Type u_1} {M : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (r s : R) (y : M),
(r - s) • y = r • y - s • y- Defined in
- Mathlib.Algebra.Module.Defs
- Cited by
- 97 results in Mathlib
- Foundations
- Depth 15 from the axioms, rests on 209 definitions · uses propext
- Assumes
- RingAddCommGroupModule
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.
- Modulestatement and proof · cited by 20,661
- AddCommGroupstatement and proof · cited by 12,871
- Ringstatement and proof · cited by 7,463
- sub_eq_add_negproof · cited by 1,023
- neg_smulproof · cited by 306
- add_smulproof · cited by 204
Cited by97
Results whose statement or proof uses this declaration.
- smul_left_injectiveproof · cited by 25
- linearIndependent_iff'proof · cited by 22
- AffineMap.lineMap_apply_moduleproof · cited by 16
- RootPairing.setOfPred_root_add_zsmul_eq_Icc_of_linearIndependentproof · cited by 5
- toIocDiv_add_zsmul'proof · cited by 5
- toIocMod_add_zsmul'proof · cited by 5
- toIcoDiv_add_zsmul'proof · cited by 5
- toIcoMod_add_zsmul'proof · cited by 5
- Affine.Simplex.point_vsub_centroid_eq_smul_vsubproof · cited by 4
- IsLocalization.away_of_isIdempotentElemproof · cited by 4
- LieAlgebra.IsKilling.apply_coroot_eq_cast'proof · cited by 4
- intervalIntegral.integral_const'proof · cited by 3