conj_pow — Mathlib

English

Let M be a monoid. If u is a unit in M and x ∈ M, then for all n ∈ ℕ, the conjugate of x by u raised to the n-th power equals the conjugate by u of x^n: (u x u^{-1})^n = u x^n u^{-1}.

Русский

Пусть M — моноид. Пусть u— единичный элемент M и x ∈ M. Тогда для любого n ∈ ℕ выполняется: (u x u^{-1})^n = u x^n u^{-1}.

LaTeX

$$$(u x u^{-1})^n = u\,x^n\,u^{-1}$$$

Lean4

theorem conj_pow (u : Mˣ) (x : M) (n : ℕ) : ((↑u : M) * x * (↑u⁻¹ : M)) ^ n = (u : M) * x ^ n * (↑u⁻¹ : M) :=
  eq_divp_iff_mul_eq.2 ((u.mk_semiconjBy x).pow_right n).eq.symm

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