Theorems · Theorem · group theory
zero_nsmul
∀ {M : Type u_2} [inst : AddMonoid M] (a : M), 0 • a = 0- Defined in
- Mathlib.Algebra.Group.Defs
- Cited by
- 137 results in Mathlib
- Foundations
- Depth 6 from the axioms, rests on 34 definitions · uses no axioms
- Assumes
- AddMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddMonoidstatement and proof · cited by 2,864
- AddMonoid.nsmul_zeroproof · cited by 1
Cited by138
Results whose statement or proof uses this declaration.
- nsmul_eq_mulproof · cited by 369
- one_nsmulproof · cited by 63
- neg_zsmulproof · cited by 41
- add_zsmulproof · cited by 21
- List.sum_replicateproof · cited by 19
- add_one_zsmulproof · cited by 19
- Nat.factorization_powproof · cited by 17
- addOrderOf_dvd_iff_nsmul_eq_zeroproof · cited by 17
- AddMonoid.exponent_nsmul_eq_zeroproof · cited by 12
- Multiset.count_nsmulproof · cited by 10
- Function.Periodic.nsmulproof · cited by 9
- Finset.coe_nsmulproof · cited by 9