instSMulCommClass_sphere_closedBall_ball

English

The scalar actions from sphere on ball commute with ball's internal scalar action.

Русский

Скалярные действия сферы на шар коммутируют с внутренними скалярными действиями шара.

LaTeX

$$$\text{instSMulCommClass_sphere_ball_ball}$$$

Lean4

instance instSMulCommClass_sphere_closedBall_ball :
    SMulCommClass (sphere (0 : 𝕜) 1) (closedBall (0 : 𝕜') 1) (ball (0 : E) r) :=
  ⟨fun a b c => Subtype.ext <| smul_comm (a : 𝕜) (b : 𝕜') (c : E)⟩

Похожие утверждения