mul_zpow

Mathlib.Algebra.Group.Basic

URI: https://scilib.ai/kg/mathlib#mul_zpow

← MathLib Explorer

English

For all integers n, (a * b)ⁿ = aⁿ * bⁿ.

Русский

Для любого целого n верно: (a b)ⁿ = aⁿ bⁿ.

LaTeX

$$$ (a \cdot b)^{n} = a^{n} \cdot b^{n} \quad (n \in \mathbb{Z}) $$$

Lean4

@[to_additive zsmul_add]
theorem mul_zpow : ∀ n : ℤ, (a * b) ^ n = a ^ n * b ^ n
  | (n : ℕ) => by simp_rw [zpow_natCast, mul_pow]
  | .negSucc n => by simp_rw [zpow_negSucc, ← inv_pow, mul_inv, mul_pow]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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