isSMulRegular_iff_right_eq_zero_of_smul

English

IsSMulRegular M r iff ∀ m ∈ M, r • m = 0 → m = 0

Русский

IsSMulRegular M r эквивалентно тому, что для всех m в M, r • m = 0 ⇒ m = 0

LaTeX

$$theorem isSMulRegular_iff_right_eq_zero_of_smul : IsSMulRegular M r ↔ ∀ m : M, r • m = 0 → m = 0$$

Lean4

theorem isSMulRegular_iff_right_eq_zero_of_smul [AddGroup M] [DistribSMul R M] {r : R} :
    IsSMulRegular M r ↔ ∀ m : M, r • m = 0 → m = 0
    where
  mp h _ := h.right_eq_zero_of_smul
  mpr h m₁ m₂ eq := sub_eq_zero.mp <| h _ <| by simp_rw [smul_sub, eq, sub_self]

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