pow_mul_comm

Mathlib.Algebra.Group.Defs

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

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem pow_mul_comm (a : M) (m n : ℕ) : a ^ m * a ^ n = a ^ n * a ^ m := by rw [← pow_add, ← pow_add, Nat.add_comm]

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

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

Разделы

Аффилиация

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