Theorems · Theorem · group theory
neg_nsmul
∀ {α : Type u_1} [inst : SubtractionMonoid α] (a : α) (n : ℕ), n • -a = -(n • a)- Defined in
- Mathlib.Algebra.Group.Basic
- Cited by
- 19 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses propext
- Assumes
- SubtractionMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- SubtractionMonoidstatement and proof · cited by 208
Cited by19
Results whose statement or proof uses this declaration.
- mul_zsmul'proof · cited by 16
- zsmul_negproof · cited by 6
- zsmul_addproof · cited by 3
- abs_nsmulproof · cited by 3
- nsmul_mem_ballproof · cited by 2
- nsmul_subproof · cited by 2
- isOfFinAddOrder_neg_iffproof · cited by 2
- addOrderOf_negproof · cited by 2
- Finset.pluennecke_ruzsa_inequality_nsmul_sub_nsmul_subproof · cited by 1
- IsTopologicalAddGroup.exist_openAddSubgroup_sub_clopen_nhds_of_zeroproof · cited by 1
- sub_nsmul_negproof · cited by 0
- Filter.Tendsto.atTop_nsmul_neg_constproof · cited by 0