pow_toProd

Mathlib.Analysis.CStarAlgebra.Multiplier

URI: https://scilib.ai/kg/mathlib#DoubleCentralizer.pow_toProd

English

Another routine compatibility relation for powers with the product representation.

Русский

Ещё одно обычное отношение совместимости степеней со структурой произведения.

LaTeX

$$$ (a^n).toProd = a.toProd^n$$$

Lean4

@[simp]
theorem pow_toProd (n : ℕ) (a : 𝓜(𝕜, A)) : (a ^ n).toProd = a.toProd ^ n :=
  rfl

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

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

Разделы

Аффилиация

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