α : Type u_1
β : Type ?u.44527
γ : Type ?u.44530
ι : Type ?u.44533
inst✝ : NonUnitalSeminormedRing α
x y : α
⊢ ‖↑(AddMonoidHom.mulRight x) y‖ ≤ ‖y‖ * ‖x‖
α : Type u_1
β : Type ?u.44527
γ : Type ?u.44530
ι : Type ?u.44533
inst✝ : NonUnitalSeminormedRing α
x y : α
⊢ ‖↑(AddMonoidHom.mulRight x) y‖ ≤ ‖x‖ * ‖y‖
rw [mul_comm]
no goals
α : Type u_1
β : Type ?u.44527
γ : Type ?u.44530
ι : Type ?u.44533
inst✝ : NonUnitalSeminormedRing α
x y : α
⊢ ‖↑(AddMonoidHom.mulRight x) y‖ ≤ ‖y‖ * ‖x‖
exact norm_mul_le y x