Theorems · Theorem · group theory
smul_neg
∀ {M : Type u_1} {A : Type u_7} [inst : AddGroup A] [inst_1 : DistribSMul M A] (r : M) (x : A), r • -x = -(r • x)- Cited by
- 181 results in Mathlib
- Foundations
- Depth 12 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.
Cites6
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
- smul_zeroproof · cited by 665
- smul_addproof · cited by 263
- neg_add_cancelproof · cited by 256
- DistribSMulstatement and proof · cited by 117
- eq_neg_of_add_eq_zero_leftproof · cited by 21
Cited by181
Results whose statement or proof uses this declaration.
- smul_subproof · cited by 142
- neg_convexOn_iffproof · cited by 10
- realPart_add_I_smul_imaginaryPartproof · cited by 10
- neg_smul_negproof · cited by 9
- slope_commproof · cited by 9
- sameRay_neg_iffproof · cited by 8
- Orientation.oangle_smul_right_of_negproof · cited by 7
- LieAlgebra.IsKilling.chainBotCoeff_add_chainTopCoeffproof · cited by 6
- Sbtw.angle₁₂₃_eq_piproof · cited by 6
- EuclideanGeometry.angle_eq_pi_iff_sbtwproof · cited by 6
- LieAlgebra.IsKilling.exists_isSl2Triple_of_weight_isNonZeroproof · cited by 5
- Matrix.det_eq_sign_charpoly_coeffproof · cited by 5