unitSphereToUnits_apply_coe — Mathlib

English

The image of a unit sphere element under the homomorphism, when viewed as a scalar, equals the original scalar.

Русский

Образ элемента единичной сферы под гомоморфизмом, взятый как скаляр, равен исходному скаляру.

LaTeX

$$$(unitSphereToUnits 𝕜 x : 𝕜) = x$ for $x \in S$$$

Lean4

@[simp]
theorem unitSphereToUnits_apply_coe [NormedDivisionRing 𝕜] (x : sphere (0 : 𝕜) 1) : (unitSphereToUnits 𝕜 x : 𝕜) = x :=
  rfl

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