zsmul — Mathlib

English

Integer scalar action on quotient by a subtraction-friendly structure.

Русский

Целочисленное скалярное действие на факторе в контексте группы вычитания.

LaTeX

$$$\\mathbb{Z}$-smul on $c.Quotient$$$

Lean4

/-- The integer scaling induced on the quotient by a congruence relation on a type with a
subtraction. -/
instance _root_.AddCon.Quotient.zsmul {M : Type*} [AddGroup M] (c : AddCon M) : SMul ℤ c.Quotient :=
  ⟨fun z => (Quotient.map' (z • ·)) fun _ _ => c.zsmul z⟩

Похожие утверждения