instTwoUniqueSumsOfModuleRat — Mathlib

English

Every vector space over the rational numbers ℚ has the TwoUniqueSums property.

Русский

Каждое пространство над полем рациональных чисел ℚ обладает свойством TwoUniqueSums.

LaTeX

$$$\forall G\;\big(\text{AddCommGroup}(G) \wedge \text{Module}\;\mathbb{Q}\, G\big) \Rightarrow \text{TwoUniqueSums}(G)$$$

Lean4

/-- Any `ℚ`-vector space has `TwoUniqueSums`, because it is isomorphic to some
  `(Basis.ofVectorSpaceIndex ℚ G) →₀ ℚ` by choosing a basis, and `ℚ` already has
  `TwoUniqueSums` because it's ordered. -/
instance [AddCommGroup G] [Module ℚ G] : TwoUniqueSums G :=
  TwoUniqueSums.of_injective_addHom _ (Module.Basis.ofVectorSpace ℚ G).repr.injective inferInstance

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