Theorems · Theorem · commutative algebra
Int.cast_smul_eq_zsmul
∀ (R : Type u_1) {M : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (n : ℤ) (b : M),
↑n • b = n • bzsmul is equal to any other module structure via a cast.
- Defined in
- Mathlib.Algebra.Module.NatInt
- Cited by
- 28 results in Mathlib
- Foundations
- Depth 40 from the axioms · uses propext
- Assumes
- RingAddCommGroupModule
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
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
- AddCommGroupstatement and proof · cited by 12,871
- Ringstatement and proof · cited by 7,463
- Nat.cast_oneproof · cited by 2,501
- one_smulproof · cited by 1,374
- Nat.cast_addproof · cited by 586
- Int.cast_natCastproof · cited by 393
- neg_smulproof · cited by 306
- neg_add_revproof · cited by 236
- add_smulproof · cited by 204
- Nat.cast_smul_eq_nsmulproof · cited by 110
- negSucc_zsmulproof · cited by 45
Cited by28
Results whose statement or proof uses this declaration.
- TensorProduct.gradedComm_of_tmul_ofproof · cited by 5
- ZLattice.rankproof · cited by 5
- TensorProduct.tmul_of_gradedMul_of_tmulproof · cited by 5
- map_intCast_smulproof · cited by 3
- LieAlgebra.Basis.linearIndependent_baseSuppproof · cited by 3
- ZSpan.repr_floor_applyproof · cited by 3
- LieAlgebra.Basis.baseSupp_apply_smul_eproof · cited by 3
- IsSl2Triple.HasPrimitiveVectorWith.pow_toEnd_f_ne_zero_of_eq_natproof · cited by 2
- RootPairing.EmbeddedG2.allRoots_eq_map_allCoeffsproof · cited by 2
- GradedTensorProduct.tmul_coe_mul_coe_tmulproof · cited by 2
- Rep.standardComplex.d_eqproof · cited by 1
- RootPairing.Base.eq_one_or_neg_one_of_mem_support_of_smul_mem_auxproof · cited by 1