Theorems · Theorem · commutative algebra
zsmul_eq_mul
∀ {α : Type u_3} [inst : NonAssocRing α] (a : α) (n : ℤ), n • a = ↑n * a- Defined in
- Mathlib.Data.Int.Cast.Lemmas
- Cited by
- 120 results in Mathlib
- Foundations
- Depth 16 from the axioms, rests on 202 definitions · uses propext
- Assumes
- NonAssocRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- one_mulproof · cited by 2,841
- neg_mulproof · cited by 654
- NonAssocRingstatement and proof · cited by 483
- Int.cast_natCastproof · cited by 393
- nsmul_eq_mulproof · cited by 369
- add_mulproof · cited by 363
- neg_add_revproof · cited by 236
- natCast_zsmulproof · cited by 118
- Nat.cast_succproof · cited by 99
- negSucc_zsmulproof · cited by 45
- Int.cast_negSuccproof · cited by 32
Cited by120
Results whose statement or proof uses this declaration.
- Function.Periodic.int_mulproof · cited by 18
- Matrix.det_apply'proof · cited by 11
- fourier_coe_applyproof · cited by 7
- Complex.arg_mem_Iocproof · cited by 6
- Matrix.det_permuteproof · cited by 6
- AddCircle.norm_eqproof · cited by 6
- RootPairing.setOfPred_root_add_zsmul_eq_Icc_of_linearIndependentproof · cited by 5
- Subgroup.strictPeriods_eq_zmultiples_one_of_T_memproof · cited by 4
- AddCircle.injective_toCircleproof · cited by 4
- Real.Angle.toReal_injectiveproof · cited by 4
- LieAlgebra.IsKilling.rootSpace_neg_nsmul_add_chainTop_of_ltproof · cited by 3
- LieAlgebra.Basis.baseSupp_apply_h'proof · cited by 3