noZeroSMulDivisors_iff_right_eq_zero_of_smul

English

NoZeroSMulDivisors R M is equivalent to the property that for all r ≠ 0 and all m ∈ M, r • m = 0 implies m = 0.

Русский

NoZeroSMulDivisors R M эквивалентно свойству: для всех r ≠ 0 и всех m ∈ M, если r • m = 0, то m = 0.

LaTeX

$$NoZeroSMulDivisors R M ↔ ∀ r : R, r ≠ 0 → ∀ m : M, r • m = 0 → m = 0$$

Lean4

theorem noZeroSMulDivisors_iff_right_eq_zero_of_smul [Zero R] [Zero M] [SMul R M] :
    NoZeroSMulDivisors R M ↔ ∀ r : R, r ≠ 0 → ∀ m : M, r • m = 0 → m = 0 :=
  by
  simp_rw [noZeroSMulDivisors_iff, or_iff_not_imp_left]
  exact ⟨fun h r hr m eq ↦ h eq hr, fun h r m eq hr ↦ h r hr m eq⟩

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