nsmul — Mathlib

English

There is a natural-scalar action on the quotient c.Quotient by n ∈ ℕ defined by [x] ↦ [n • x].

Русский

На фактор-модуле по конгруэнции c действует скалярами из ℕ: n • [x] = [n • x].

LaTeX

$$$\\text{There exists an action }\\mathrm{SMul}_\\mathbb{N} : \\mathbb{N} \\curvearrowright c.\\Quotient\\;\\text{defined by } n\\cdot [x] = [n\\cdot x]$$$

Lean4

instance _root_.AddCon.Quotient.nsmul {M : Type*} [AddMonoid M] (c : AddCon M) : SMul ℕ c.Quotient where
  smul n := (Quotient.map' (n • ·)) fun _ _ => c.nsmul n

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