Theorems · Theorem · commutative algebra
neg_smul
∀ {R : Type u_1} {M : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (r : R) (x : M),
-r • x = -(r • x)- Defined in
- Mathlib.Algebra.Module.Defs
- Cited by
- 306 results in Mathlib
- Foundations
- Depth 14 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.
Cites7
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
- zero_smulproof · cited by 716
- neg_add_cancelproof · cited by 256
- add_smulproof · cited by 204
- eq_neg_of_add_eq_zero_leftproof · cited by 21
Cited by306
Results whose statement or proof uses this declaration.
- sub_smulproof · cited by 97
- Int.cast_smul_eq_zsmulproof · cited by 28
- Units.neg_smulproof · cited by 27
- neg_one_smulproof · cited by 23
- realPart_add_I_smul_imaginaryPartproof · cited by 10
- groupCohomology.comp_d₁₂_eqproof · cited by 10
- groupHomology.comp_d₂₁_eqproof · cited by 10
- neg_smul_negproof · cited by 9
- slope_commproof · cited by 9
- MeromorphicAt.negproof · cited by 8
- Orientation.oangle_smul_right_of_negproof · cited by 7
- RootPairing.Base.exists_root_eq_sum_intproof · cited by 7
Showing the 200 most cited of 306.