ZPow — Mathlib

English

There is a natural integer-power operation on Set α via zpow, combining nat-pow with inverses.

Русский

Существует целочисленное возведение множества в степень: S^z определено через произведение и обращения элементов.

LaTeX

$$$$ S^z = \begin{cases} S^n & z=n \ge 0 \\ (S^{-1})^{|z|} & z<0 \end{cases}, \quad S^{-1} = \{ x^{-1} \mid x \in S \}. $$$$

Lean4

/-- Repeated pointwise multiplication/division (not the same as pointwise repeated
multiplication/division!) of a `Set`. See note [pointwise nat action]. -/
@[to_additive existing]
protected def ZPow [One α] [Mul α] [Inv α] : Pow (Set α) ℤ :=
  ⟨fun s n => zpowRec npowRec n s⟩

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