subsingleton_nnrat_module — Mathlib

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⟩

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