isScalarTower_sphere_ball_ball — Mathlib

English

The scalar actions on the sphere and ball commute with the action on the ball, yielding a commuting scalar action structure.

Русский

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

LaTeX

$$$\text{instSMulCommClass_sphere_closedBall_closedBall}$$$

Lean4

instance isScalarTower_sphere_ball_ball : IsScalarTower (sphere (0 : 𝕜) 1) (ball (0 : 𝕜') 1) (ball (0 : 𝕜') 1) :=
  ⟨fun a b c => Subtype.ext <| smul_assoc (a : 𝕜) (b : 𝕜') (c : 𝕜')⟩

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