pow_mul'

Mathlib.Algebra.Group.Defs

URI: https://scilib.ai/kg/mathlib#pow_mul'

English

For a ∈ M and m,n ∈ ℕ, a^{m n} = (a^{n})^{m}.

Русский

Для a ∈ M и m,n ∈ ℕ верно a^{m n} = (a^{n})^{m}.

LaTeX

$$$a^{m n} = (a^{n})^{m}$$$

Lean4

@[to_additive mul_nsmul']
theorem pow_mul' (a : M) (m n : ℕ) : a ^ (m * n) = (a ^ n) ^ m := by rw [Nat.mul_comm, pow_mul]

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

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

Разделы

Аффилиация

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