mul_left_coe_nonZeroDivisors_eq_zero_iff

English

If c is a nonzero-divisor in M, then left multiplication by c is left-canceling: c x = 0 iff x = 0.

Русский

Если c является ненулевым делителем, левая умножение на c образует нулевой результат тогда и только тогда, когда x = 0.

LaTeX

$$mul_left_coe_nonZeroDivisors_eq_zero_iff {c : M0⁰} : (c : M0) * x = 0 ↔ x = 0$$

Lean4

@[simp]
theorem mul_left_coe_nonZeroDivisors_eq_zero_iff {c : M₀⁰} : (c : M₀) * x = 0 ↔ x = 0 :=
  mul_left_mem_nonZeroDivisors_eq_zero_iff c.prop

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