coe_smul

Mathlib.Algebra.Star.Unitary

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

English

The coercion intertwines the smul on unitary elements: the underlying element of r • a equals the action of r on a.

Русский

Сведение сохраняет скалярное умножение: подлежащее (коэрц) фиксирует, что ↑(r • a) = r • a.

LaTeX

$$$\\uparrow (r \\cdot a) = r \\cdot (a)$$$

Lean4

@[simp, norm_cast]
theorem coe_smul (r : unitary R) (a : unitary A) : ↑(r • a) = r • (a : A) :=
  rfl

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

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

Разделы

Аффилиация

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