npow — Mathlib

English

There is a natural-power operation on Finset α, defined by repeated pointwise multiplication of Finsets.

Русский

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

LaTeX

$$$$ \\text{Finset }\\alpha \\text{ is closed under } \\cdot \\text{-multiplication by taking pairwise products } ;$$$$

Lean4

/-- Repeated pointwise multiplication (not the same as pointwise repeated multiplication!) of a
`Finset`. See note [pointwise nat action]. -/
protected def npow [One α] [Mul α] : Pow (Finset α) ℕ :=
  ⟨fun s n => npowRec n s⟩

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