uniqueNatModule — Mathlib

English

There exists a unique ℕ-module structure on any AddCommMonoid M; in other words, all ℕ-module structures on M coincide.

Русский

Существует единственная структура модуля над ℕ на любой AddCommMonoid M; то есть все ℕ-модули на M совпадают.

LaTeX

$$$\\mathrm{Unique} (\\mathrm{Module}\\ \\mathbb{N} \\ M)$$$

Lean4

/-- All `ℕ`-module structures are equal. Not an instance since in mathlib all `AddCommMonoid`
should normally have exactly one `ℕ`-module structure by design. -/
def uniqueNatModule : Unique (Module ℕ M) where
  default := inferInstance
  uniq P := (Module.ext' P _) fun n => by convert nat_smul_eq_nsmul P n

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