conj_pow' — Mathlib

English

Let M be a monoid. If u is a unit in M and x ∈ M, then for all n ∈ ℕ, ((u^{-1}) x u)^n = u^{-1} x^n u.

Русский

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

LaTeX

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

Lean4

theorem conj_pow' (u : Mˣ) (x : M) (n : ℕ) : ((↑u⁻¹ : M) * x * (u : M)) ^ n = (↑u⁻¹ : M) * x ^ n * (u : M) :=
  u⁻¹.conj_pow x n

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