smulRight_zero — Mathlib

English

If no zero smul divisors hold in S acting on M, then f.smulRight x = 0 implies f = 0 or x = 0 (under NoZeroSMulDivisors S M).

Русский

Если в действии S на M отсутствуют нулевые делители по умножению, то f.smulRight x = 0 влечет f = 0 или x = 0 (при условии NoZeroSMulDivisors S M).

LaTeX

$$f.smulRight x = 0 \iff f = 0 \lor x = 0$$

Lean4

@[simp]
theorem smulRight_zero (f : M₁ →ₗ[R] S) : f.smulRight (0 : M) = 0 := by ext; simp

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