subsingleton_rat_module — Mathlib

English

There can be at most one Module Rat E structure on an additive commutative group E.

Русский

Существует не более одной структуры модуля Rat на аддитивной группе E.

LaTeX

$$$\\operatorname{Subsingleton} (\\text{Module } \\mathbb{Q} \\; E)$$$

Lean4

/-- There can be at most one `Module ℚ E` structure on an additive commutative group. -/
instance subsingleton_rat_module (E : Type*) [AddCommGroup E] : Subsingleton (Module ℚ E) :=
  ⟨fun P Q => (Module.ext' P Q) fun r x => map_rat_smul (_instM := P) (_instM₂ := Q) (AddMonoidHom.id E) r x⟩

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