noZeroSMulDivisors — Mathlib

English

There is a NoZeroSmulDivisors for ℕ on an AddCommMonoid M with a ℚ≥0-module structure; if k ∈ ℕ and k • x = 0 then x = 0.

Русский

Существует NoZeroSmulDivisors ℕ на M с ℚ≥0-модулем: если k • x = 0, то x = 0.

LaTeX

$$$\\forall k \\in \\mathbb{N},\\; k \\cdot x = 0 \\Rightarrow x = 0$$$

Lean4

instance (priority := 100) noZeroSMulDivisors [AddCommMonoid M] [Module ℚ≥0 M] : NoZeroSMulDivisors ℕ M :=
  ⟨fun {k} {x : M} h => by simpa [← Nat.cast_smul_eq_nsmul ℚ≥0 k x] using h⟩
    -- see note [lower instance priority]

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