Theorems · Theorem · commutative algebra
ofNat_smul_eq_nsmul
∀ (R : Type u_1) {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (n : ℕ)
[inst_3 : n.AtLeastTwo] (b : M), OfNat.ofNat n • b = OfNat.ofNat n • bnsmul is equal to any other module structure via a cast.
- Defined in
- Mathlib.Algebra.Module.NatInt
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 27 from the axioms · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Modulestatement and proof · cited by 20,661
- Semiringstatement and proof · cited by 13,802
- AddCommMonoidstatement and proof · cited by 12,281
- Nat.AtLeastTwostatement and proof · cited by 405
- Nat.cast_smul_eq_nsmulproof · cited by 110
Cited by5
Results whose statement or proof uses this declaration.
- curveIntegralFun_trans_of_lt_halfproof · cited by 2
- CurveIntegrable.intervalIntegrable_curveIntegralFun_trans_leftproof · cited by 2
- CurveIntegrable.intervalIntegrable_curveIntegralFun_trans_rightproof · cited by 2
- LieAlgebra.Basis.A_diag_eq_twoproof · cited by 1
- curveIntegral_transproof · cited by 0