R : Type u_1
S : Type ?u.24255
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
h : IsSMulRegular M 0
a b : M
⊢ 0 • a = 0 • b
R : Type u_1
S : Type ?u.24255
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
h : IsSMulRegular M 0
a b : M
⊢ (fun x => 0 • x) a = (fun x => 0 • x) b
dsimp only [Function.comp]
no goals
R : Type u_1
S : Type ?u.24255
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
h : IsSMulRegular M 0
a b : M
⊢ 0 • a = 0 • b
repeat' rw [MulActionWithZero.zero_smul]
no goals
R : Type u_1
S : Type ?u.24255
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
h : IsSMulRegular M 0
a b : M
⊢ 0 = 0 • b
rw [MulActionWithZero.zero_smul]