mk_pow — Mathlib

English

If γ is a CommMonoid and ContinuousMul, α →ₘ[μ] γ inherits a CommMonoid structure with pointwise operations.

Русский

Если γ — коммутативный моноид и непрерывное умножение, то α →ₘ[μ] γ наследует структуру CommMonoid с точечными операциями.

LaTeX

$$$\text{CommMonoid}(α \to_{μ} γ)$$$

Lean4

@[simp]
theorem mk_pow (f : α → γ) (hf) (n : ℕ) :
    (mk f hf : α →ₘ[μ] γ) ^ n = mk (f ^ n) ((_root_.continuous_pow n).comp_aestronglyMeasurable hf) :=
  rfl

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