coe_pow — Mathlib

English

Under monoid structure, (f^n) corresponds to pointwise power: the underlying function of f^n is the n-th power of the underlying function f.

Русский

При моноидной структуре (f^n) является по точкам равным f^n(x).

LaTeX

$$$\\text{coe\_pow} [Monoid \\beta] (f : α \\to_{S} \\beta) (n : \\mathbb{N}) : \\⇑(f^n) = (\\⇑f)^n.$$$

Lean4

@[simp]
theorem coe_pow [Monoid β] (f : α →ₛ β) (n : ℕ) : ⇑(f ^ n) = (⇑f) ^ n :=
  rfl

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