Theorems · Theorem · group theory
zero_smul
∀ (M₀ : Type u_2) {A : Type u_7} [inst : Zero M₀] [inst_1 : Zero A] [inst_2 : SMulWithZero M₀ A] (m : A), 0 • m = 0- Cited by
- 716 results in Mathlib
- Foundations
- Depth 5 from the axioms, rests on 17 definitions · uses no axioms
- Assumes
- ZeroZeroSMulWithZero
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.
- SMulWithZerostatement and proof · cited by 113
- SMulWithZero.zero_smulproof · cited by 1
Cited by716
Results whose statement or proof uses this declaration.
- neg_smulproof · cited by 306
- Nat.cast_smul_eq_nsmulproof · cited by 110
- Finsupp.linearCombination_singleproof · cited by 90
- MeasureTheory.integral_constproof · cited by 75
- Submodule.mem_span_singletonproof · cited by 61
- inner_zero_leftproof · cited by 59
- AffineMap.lineMap_apply_zeroproof · cited by 40
- smul_eq_zeroproof · cited by 40
- Polynomial.smeval_addproof · cited by 22
- MeasureTheory.integral_smul_measureproof · cited by 22
- Module.Basis.equivFun_symm_applyproof · cited by 22
- linearIndependent_iff'proof · cited by 22
Showing the 200 most cited of 716.