normSq_zpow

Mathlib.Algebra.Quaternion

URI: https://scilib.ai/kg/mathlib#Quaternion.normSq_zpow

English

The norm is compatible with integer powers: normSq(a^z) = normSq(a)^z.

Русский

Норма совместима с целыми степенями: normSq(a^z) = normSq(a)^z.

LaTeX

$$$\operatorname{normSq}(a^{z}) = (\operatorname{normSq}(a))^{z}$$$

Lean4

theorem normSq_zpow (z : ℤ) : normSq (a ^ z) = normSq a ^ z :=
  map_zpow₀ normSq a z

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

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

Разделы

Аффилиация

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