instSMulCommClass_closedBall_closedBall_closedBall

English

Every pair of scalar actions from closedBall(0,1) and closedBall(0,1) on Ball(0,r) commute.

Русский

Любые пары скалярных действий из closedBall(0,1) и closedBall(0,1) на Ball(0,r) коммутируют.

LaTeX

$$$\text{instSMulCommClass_closedBall_closedBall_closedBall}$$$

Lean4

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

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