Theorems · Theorem · ring theory
nsmul_eq_mul
∀ {α : Type u} [inst : NonAssocSemiring α] (n : ℕ) (a : α), n • a = ↑n * a- Defined in
- Mathlib.Algebra.Ring.Defs
- Cited by
- 369 results in Mathlib
- Foundations
- Depth 11 from the axioms, rests on 116 definitions · uses no axioms
- Assumes
- NonAssocSemiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- one_mulproof · cited by 2,841
- Nat.cast_zeroproof · cited by 1,870
- MulZeroClass.zero_mulproof · cited by 1,625
- NonAssocSemiringstatement and proof · cited by 805
- add_mulproof · cited by 363
- zero_nsmulproof · cited by 137
- Nat.cast_succproof · cited by 99
- succ_nsmulproof · cited by 65
Cited by369
Results whose statement or proof uses this declaration.
- zsmul_eq_mulproof · cited by 120
- Function.Periodic.nat_mulproof · cited by 15
- Nat.smul_one_eq_castproof · cited by 13
- LieAlgebra.IsKilling.root_apply_corootproof · cited by 11
- Function.Antiperiodic.periodic_two_mulproof · cited by 10
- HasDerivAt.powproof · cited by 8
- AnalyticAt.hasFPowerSeriesAtproof · cited by 7
- Finset.sum_centroidWeights_eq_one_of_card_ne_zeroproof · cited by 6
- MvPolynomial.pderiv_powproof · cited by 6
- Polynomial.hasseDeriv_applyproof · cited by 6
- Commute.add_pow'proof · cited by 6
- Function.Periodic.sub_nat_mul_eqproof · cited by 6
Showing the 200 most cited of 369.