Results about IsSMulRegular for MonoidWithZero

theorem IsSMulRegular.subsingleton {R : Type u_1} {M : Type u_3} [MonoidWithZero R] [Zero M] [MulActionWithZero R M] (h : IsSMulRegular M 0) : Subsingleton M

The element 0 is M-regular if and only if M is trivial.

theorem IsSMulRegular.zero_iff_subsingleton {R : Type u_1} {M : Type u_3} [MonoidWithZero R] [Zero M] [MulActionWithZero R M] : IsSMulRegular M 0 ↔ Subsingleton M

The element 0 is M-regular if and only if M is trivial.

theorem IsSMulRegular.not_zero_iff {R : Type u_1} {M : Type u_3} [MonoidWithZero R] [Zero M] [MulActionWithZero R M] : ¬IsSMulRegular M 0 ↔ Nontrivial M

The 0 element is not M-regular, on a non-trivial module.

theorem IsSMulRegular.zero {R : Type u_1} {M : Type u_3} [MonoidWithZero R] [Zero M] [MulActionWithZero R M] [sM : Subsingleton M] : IsSMulRegular M 0

The element 0 is M-regular when M is trivial.

theorem IsSMulRegular.not_zero {R : Type u_1} {M : Type u_3} [MonoidWithZero R] [Zero M] [MulActionWithZero R M] [nM : Nontrivial M] : ¬IsSMulRegular M 0

The 0 element is not M-regular, on a non-trivial module.

theorem IsSMulRegular.right_eq_zero_of_smul {R : Type u_1} {M : Type u_3} [Zero M] [SMulZeroClass R M] {r : R} {x : M} (h1 : IsSMulRegular M r) (h2 : r • x = 0) : x = 0

theorem isSMulRegular_iff_right_eq_zero_of_smul {R : Type u_1} {M : Type u_3} [AddGroup M] [DistribSMul R M] {r : R} : IsSMulRegular M r ↔ ∀ (m : M), r • m = 0 → m = 0

theorem IsSMulRegular.of_right_eq_zero_of_smul {R : Type u_1} {M : Type u_3} [AddGroup M] [DistribSMul R M] {r : R} : (∀ (m : M), r • m = 0 → m = 0) → IsSMulRegular M r

Alias of the reverse direction of isSMulRegular_iff_right_eq_zero_of_smul.