mul_pow_mul

Mathlib.Algebra.Group.Defs

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem mul_pow_mul (a b : M) (n : ℕ) : (a * b) ^ n * a = a * (b * a) ^ n := by
  induction n with
  | zero => simp
  | succ n ih => simp [pow_succ', ← ih, mul_assoc]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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