unop_zpow

Mathlib.Algebra.Group.Opposite

URI: https://scilib.ai/kg/mathlib#MulOpposite.unop_zpow

English

For α with DivInvMonoid, unop(x^z) = unop x^z for x ∈ αᵐᵒᵖ and z ∈ ℤ.

Русский

Для α с DivInvMonoid верно unop(x^z) = unop x^z для x ∈ αᵐᵒᵖ и z ∈ ℤ.

LaTeX

$$$ \mathrm{unop\_zpow}(x,z):\, \mathrm{unop}(x^z) = \mathrm{unop}(x)^z $$$

Lean4

@[simp]
theorem unop_zpow (x : αᵐᵒᵖ) (z : ℤ) : unop (x ^ z) = unop x ^ z :=
  rfl

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

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

Разделы

Аффилиация

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