coe_map_star

Mathlib.Algebra.Star.Unitary

URI: https://scilib.ai/kg/mathlib#unitary.coe_map_star

English

The star-compatibility of the unitary map with star on the source is preserved under map.

Русский

Сохранение звёздной совместимости отображения unitary подмножество сохраняется при отображении.

LaTeX

$$$ map\\ f\\ (star\\ x) = star\\ (map\\ f\\ x) $$$

Lean4

@[simp]
theorem coe_map_star (f : R →⋆* S) (x : unitary R) : map f (star x) = f (star x) :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru