subsingletonIntModule — Mathlib

English

For any AddCommGroup M, the type of ℤ-module structures on M is a subsingleton; i.e. all ℤ-module structures on M are equal.

Русский

Для любого AddCommGroup M множество ℤ-модульных структур на M является подсинглтонно

LaTeX

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

Lean4

/-- All `ℤ`-module structures are equal. See also `AddCommGroup.uniqueIntModule`. -/
instance subsingletonIntModule [AddCommMonoid M] : Subsingleton (Module ℤ M) where
  allEq a
    b :=
    let : AddCommGroup M := Module.addCommMonoidToAddCommGroup ℤ
    AddCommGroup.uniqueIntModule.instSubsingleton.allEq a b

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