R : Type u_1
S : Type ?u.26076
M : Type u_2
a b : R
s : S
inst✝⁶ : MonoidWithZero R
inst✝⁵ : MonoidWithZero S
inst✝⁴ : Zero M
inst✝³ : MulActionWithZero R M
inst✝² : MulActionWithZero R S
inst✝¹ : MulActionWithZero S M
inst✝ : IsScalarTower R S M
⊢ (¬∃ x y, x ≠ y) ↔ ∀ (x y : M), x = y
R : Type u_1
S : Type ?u.26076
M : Type u_2
a b : R
s : S
inst✝⁶ : MonoidWithZero R
inst✝⁵ : MonoidWithZero S
inst✝⁴ : Zero M
inst✝³ : MulActionWithZero R M
inst✝² : MulActionWithZero R S
inst✝¹ : MulActionWithZero S M
inst✝ : IsScalarTower R S M
⊢ ¬IsSMulRegular M 0 ↔ Nontrivial M
rw [nontrivial_iff, not_iff_comm, zero_iff_subsingleton, subsingleton_iff]
R : Type u_1
S : Type ?u.26076
M : Type u_2
a b : R
s : S
inst✝⁶ : MonoidWithZero R
inst✝⁵ : MonoidWithZero S
inst✝⁴ : Zero M
inst✝³ : MulActionWithZero R M
inst✝² : MulActionWithZero R S
inst✝¹ : MulActionWithZero S M
inst✝ : IsScalarTower R S M
⊢ (∀ (x y : M), x = y) ↔ ∀ (x y : M), x = y
R : Type u_1
S : Type ?u.26076
M : Type u_2
a b : R
s : S
inst✝⁶ : MonoidWithZero R
inst✝⁵ : MonoidWithZero S
inst✝⁴ : Zero M
inst✝³ : MulActionWithZero R M
inst✝² : MulActionWithZero R S
inst✝¹ : MulActionWithZero S M
inst✝ : IsScalarTower R S M
⊢ (¬∃ x y, x ≠ y) ↔ ∀ (x y : M), x = y
push_neg
no goals
R : Type u_1
S : Type ?u.26076
M : Type u_2
a b : R
s : S
inst✝⁶ : MonoidWithZero R
inst✝⁵ : MonoidWithZero S
inst✝⁴ : Zero M
inst✝³ : MulActionWithZero R M
inst✝² : MulActionWithZero R S
inst✝¹ : MulActionWithZero S M
inst✝ : IsScalarTower R S M
⊢ (∀ (x y : M), x = y) ↔ ∀ (x y : M), x = y
exact Iff.rfl