pow_right_comm

Mathlib.Algebra.Group.Defs

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

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 nsmul_left_comm]
theorem pow_right_comm (a : M) (m n : ℕ) : (a ^ m) ^ n = (a ^ n) ^ m := by rw [← pow_mul, Nat.mul_comm, pow_mul]

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

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

Разделы

Аффилиация

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