subsingletonNatModule — Mathlib

English

For any AddCommMonoid M, the type of ℕ-module structures on M is a subsingleton; i.e., there is at most one ℕ-module structure on M.

Русский

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

LaTeX

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

Lean4

/-- All `ℕ`-module structures are equal. See also `AddCommMoniod.uniqueNatModule`. -/
instance subsingletonNatModule : Subsingleton (Module ℕ M) :=
  AddCommMonoid.uniqueNatModule.instSubsingleton

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