R : Type u_1
S : Type ?u.29294
M : Type u_2
a b : R
s : S
inst✝² : CommSemigroup R
inst✝¹ : SMul R M
inst✝ : IsScalarTower R R M
⊢ IsSMulRegular M (a * b) ↔ IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a)
R : Type u_1
S : Type ?u.29294
M : Type u_2
a b : R
s : S
inst✝² : CommSemigroup R
inst✝¹ : SMul R M
inst✝ : IsScalarTower R R M
⊢ IsSMulRegular M (a * b) ↔ IsSMulRegular M a ∧ IsSMulRegular M b
rw [← mul_and_mul_iff]
no goals
R : Type u_1
S : Type ?u.29294
M : Type u_2
a b : R
s : S
inst✝² : CommSemigroup R
inst✝¹ : SMul R M
inst✝ : IsScalarTower R R M
⊢ IsSMulRegular M (a * b) ↔ IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a)
exact ⟨fun ab => ⟨ab, by rwa [mul_comm]⟩, fun rab => rab.1⟩
no goals
R : Type u_1
S : Type ?u.29294
M : Type u_2
a b : R
s : S
inst✝² : CommSemigroup R
inst✝¹ : SMul R M
inst✝ : IsScalarTower R R M
ab : IsSMulRegular M (a * b)
⊢ IsSMulRegular M (b * a)
rwa [mul_comm]