conj_pow₀

Mathlib.Algebra.GroupWithZero.Conj

URI: https://scilib.ai/kg/mathlib#GroupWithZero.conj_pow₀

← MathLib Explorer

English

If a ≠ 0, then (a^{-1} d a)^s = a^{-1} d^{s} a for s ∈ ℕ.

Русский

Если a ≠ 0, то (a^{-1} d a)^s = a^{-1} d^{s} a для любого s ∈ ℕ.

LaTeX

$$$a \neq 0 \Rightarrow (a^{-1} d a)^s = a^{-1} d^{s} a$$$

Lean4

theorem conj_pow₀ {s : ℕ} {a d : α} (ha : a ≠ 0) : (a⁻¹ * d * a) ^ s = a⁻¹ * d ^ s * a :=
  let u : αˣ := ⟨a, a⁻¹, mul_inv_cancel₀ ha, inv_mul_cancel₀ ha⟩
  Units.conj_pow' u d s

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

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

Разделы

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

Аффилиация

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