coe_pow — Mathlib

English

The coercion commutes with powering: the function underlying f^n equals the n-th power of the function underlying f.

Русский

Приведение к функциям commute с возведением в степень: функция, лежащая в f^n, равна (f)^n.

LaTeX

$$ [Monoid β] [ContinuousMul β] (f : C(α, β)) (n : Nat) : ⇑(f ^ n) = (⇑f) ^ n$$

Lean4

@[to_additive (attr := norm_cast) (reorder := 7 8)]
theorem coe_pow [Monoid β] [ContinuousMul β] (f : C(α, β)) (n : ℕ) : ⇑(f ^ n) = (⇑f) ^ n :=
  rfl

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