instIsAddTorsionFreeOfModuleNNRat

English

There exists a structure making a module over NN Rat torsion-free, i.e., for which n·x = 0 implies x = 0 for nonzero n.

Русский

Существует структура модуля над NN Rat, тождественная свободному от torsion, то есть если n·x = 0 и n ≠ 0, тогда x = 0.

LaTeX

$$$\text{IsAddTorsionFree } R$ for NN Rat module$$

Lean4

local instance {R : Type*} [AddCommMonoid R] [Module ℚ≥0 R] : IsAddTorsionFree R where
  nsmul_right_injective {n} hn r s
    hrs := by
    rw [← one_smul ℚ≥0 r, ← one_smul ℚ≥0 s, show 1 = (n : ℚ≥0)⁻¹ • (n : ℚ≥0) by simp_all]
    simp_all only [smul_assoc, Nat.cast_smul_eq_nsmul]

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