smul_eq_zero — Mathlib

English

Let R be a ring with zero and M a left R-module with scalar multiplication having no zero divisors. Then for all c in R and x in M, c · x = 0 if and only if c = 0 or x = 0.

Русский

Пусть R — кольцо с нулём и M — модуль над R, на котором скалярное умножение не имеет делителей нуля. Тогда для любых c ∈ R и x ∈ M выполняется c · x = 0 тогда и только тогда, когда c = 0 или x = 0.

LaTeX

$$$$\forall c \in R, \forall x \in M, c \cdot x = 0 \iff c = 0 \lor x = 0.$$$$

Lean4

@[simp]
theorem smul_eq_zero : c • x = 0 ↔ c = 0 ∨ x = 0 :=
  ⟨eq_zero_or_eq_zero_of_smul_eq_zero, fun h => h.elim (fun h => h.symm ▸ zero_smul R x) fun h => h.symm ▸ smul_zero c⟩

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