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⟩