zpow — Mathlib

English

There is an integer-exponentiation operation on Finset α, defined via the corresponding bi-operations.

Русский

Существует операция возведения в целочисленную степень над Finset α, задаваемая через соответствующие операции.

LaTeX

$$$$ \\text{Finset }\\alpha \\text{ has } \\mathbb{Z}\\text{-powered structure by } \\cdot \\text{ and } ^{-1} $$$$

Lean4

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

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