pow_inv_comm₀

Mathlib.Algebra.GroupWithZero.Commute

URI: https://scilib.ai/kg/mathlib#pow_inv_comm₀

English

For any a in GroupWithZero and natural numbers m,n, a^{-1}^{m} a^{n} = a^{n} a^{-1}^{m}.

Русский

Для любого a в GroupWithZero и натуральных m,n верно a^{-1}^{m} a^{n} = a^{n} a^{-1}^{m}.

LaTeX

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

Lean4

theorem pow_inv_comm₀ (a : G₀) (m n : ℕ) : a⁻¹ ^ m * a ^ n = a ^ n * a⁻¹ ^ m :=
  (Commute.refl a).inv_left₀.pow_pow m n

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

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

Разделы

Аффилиация

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