pow_mul_comm'

Mathlib.Algebra.Group.Defs

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

English

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

Русский

Для a ∈ M и n ∈ ℕ выполняется a^{n} a = a a^{n}.

LaTeX

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

Lean4

@[to_additive]
theorem pow_mul_comm' (a : M) (n : ℕ) : a ^ n * a = a * a ^ n := by rw [← pow_succ, pow_succ']

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

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

Разделы

Аффилиация

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