two_nsmul_eq_zero — Mathlib

English

Let R be a ring/semiring and M an NoZeroSMulDivisors R M module; then for any v ∈ M, 2v = 0 iff v = 0.

Русский

Пусть R — кольцо (полукольцо), M — модуль с NoZeroSMulDivisors R M; тогда для любого v ∈ M, 2v = 0 эквивалентно v = 0.

LaTeX

$$∀ v ∈ M, 2 · v = 0 ⇔ v = 0$$

Lean4

theorem two_nsmul_eq_zero (R) (M) [Semiring R] [CharZero R] [AddCommMonoid M] [Module R M] [NoZeroSMulDivisors R M]
    {v : M} : 2 • v = 0 ↔ v = 0 := by
  haveI := Nat.noZeroSMulDivisors R M
  simp [smul_eq_zero]

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