Theorems · Theorem · group theory
nsmul_add
∀ {M : Type u_4} [inst : AddCommMonoid M] (a b : M) (n : ℕ), n • (a + b) = n • a + n • b- Defined in
- Mathlib.Algebra.Group.Basic
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses propext
- Assumes
- AddCommMonoid
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.
- AddCommMonoidstatement and proof · cited by 12,281
Cited by13
Results whose statement or proof uses this declaration.
- nsmulAddMonoidHomproof · cited by 24
- zsmul_addproof · cited by 3
- nsmul_mem_ballproof · cited by 2
- nsmul_subproof · cited by 2
- LieModule.toEnd_pow_lieproof · cited by 1
- Multiset.nsmul_consproof · cited by 1
- nsmul_mem_closedBallproof · cited by 0
- Multiset.filter_nsmulproof · cited by 0
- two_nsmul_lie_lmul_lmul_add_add_eq_zeroproof · cited by 0
- two_nsmul_lie_lmul_lmul_add_eq_lie_lmul_lmul_addproof · cited by 0
- Finset.sum_Icc_of_even_eq_rangeproof · cited by 0
- AddCommGroup.ModEq.nsmulproof · cited by 0