gelfandTransform_map_star — Mathlib

English

The Gelfand transform commutes with the star operation: gelfandTransform(★a) = ★(gelfandTransform(a)).

Русский

Гельфанд-преобразование сохраняет звёздочный инволюцию: gelfandTransform(звезда a) = звезда( gelfandTransform(a) ).

LaTeX

$$$$gelfandTransform(\star a) = \star( gelfandTransform(a) )$$$$

Lean4

theorem gelfandTransform_map_star (a : A) : gelfandTransform ℂ A (star a) = star (gelfandTransform ℂ A a) :=
  ContinuousMap.ext fun φ => map_star φ a

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