coe_mul — Mathlib

English

The embedding preserves multiplication on the unit sphere: the image of the product is the product of images.

Русский

Вложение сохраняет умножение на единичной сфере: изображение произведения равно произведению изображений.

LaTeX

$$$\uparrow(xy) = \uparrow x \cdot \uparrow y$ for $x,y \in S$$$

Lean4

@[simp, norm_cast]
theorem coe_mul [SeminormedRing 𝕜] [NormMulClass 𝕜] [NormOneClass 𝕜] (x y : sphere (0 : 𝕜) 1) :
    ↑(x * y) = (x * y : 𝕜) :=
  rfl

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