pow_toGerm — Mathlib

English

The monoid structure on AEEqFun is compatible with the map to Germ and the existing monoid axioms (identity, multiplication, power).

Русский

Структура моноида на AEEqFun совместима с отображением в Germ и аксиомами моноида (тождество, умножение, степенная операция).

LaTeX

$$$\text{Monoid}(AEEqFun) \Rightarrow \text{compatibility with germ and axioms}$$$

Lean4

@[simp]
theorem pow_toGerm (f : α →ₘ[μ] γ) (n : ℕ) : (f ^ n).toGerm = f.toGerm ^ n :=
  comp_toGerm _ _ _

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