isScalarTower_sphere_sphere_sphere

English

The scalar multiplications coming from the ball and sphere commute on the ball, i.e., actions from distinct scalar sets commute.

Русский

Действия, вызываемые шарами и шарами, коммутируют на шаре; действия от разных скаляров commute.

LaTeX

$$$\text{SMulCommClass}(\text{closedBall}(0,1),\ \text{closedBall}(0,1),\ \text{ball}(0,r))$$$

Lean4

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

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