toZPow

Mathlib.Algebra.Group.Defs

URI: https://scilib.ai/kg/mathlib#DivInvMonoid.toZPow

English

In a DivInvMonoid M, there is an integer-exponent power operation x^n with n ∈ ℤ.

Русский

В DivInvMonoid M существует операция возведения в целые степени: x^n, где n ∈ ℤ.

LaTeX

$$$\\forall x \\in M, \\forall n \\in \\mathbb{Z},\\ x^{n} \\text{ defined as integer exponentiation}$$$

Lean4

instance toZPow {M} [DivInvMonoid M] : Pow M ℤ :=
  ⟨fun x n ↦ DivInvMonoid.zpow n x⟩

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

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

Разделы

Аффилиация

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