Mathlib Map

Theorems · Definition · group theory

ZSMul.zsmul

{G : Type u} → [self : ZSMul G] → ℤ → G → G

Multiplication by an integer. Set this to zsmulRec unless Module diamonds are possible.

Defined in
Mathlib.Algebra.Group.Defs
Cited by
8 results in Mathlib
Foundations
Depth 1 from the axioms · uses no axioms
Assumes
ZSMul
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

SubNegMonoid.ext · cited by 2SubNegMonoid.extLeftPreLieRing.ext · cited by 1LeftPreLieRing.extLieAdmissibleRing.ext · cited by 1LieAdmissibleRing.extRightPreLieRing.ext · cited by 1RightPreLieRing.extzsmul_eq_smul · cited by 0zsmul_eq_smulLeftPreLieRing.ext_iff · cited by 0LeftPreLieRing.ext_iffLieAdmissibleRing.ext_iff · cited by 0LieAdmissibleRing.ext_iffRightPreLieRing.ext_iff · cited by 0RightPreLieRing.ext_iffZSMul · cited by 3ZSMulZSMul.zsmulCITED BYCITES

Cites1

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • ZSMulstatement and proof · cited by 3

Cited by8

Results whose statement or proof uses this declaration.