English
There can be at most one Module ℚ≥0 E structure on an additive commutative monoid E.
Русский
Существует не более одной структуры модуля ℚ≥0 на добавочной коммутативной моноиде E.
LaTeX
$$$\\operatorname{Subsingleton} (\\text{Module } \\mathbb{Q}_{\\ge 0} E)$$$
Lean4
/-- There can be at most one `Module ℚ≥0 E` structure on an additive commutative monoid. -/
instance subsingleton_nnrat_module (E : Type*) [AddCommMonoid E] : Subsingleton (Module ℚ≥0 E) :=
⟨fun P Q => (Module.ext' P Q) fun r x => map_nnrat_smul (_instM := P) (_instM₂ := Q) (AddMonoidHom.id E) r x⟩