apply_mint — Mathlib

English

For f: Multiplicative ℤ →* α, and n ∈ Multiplicative ℤ, f(n) equals f(ofAdd 1) raised to the power n.toAdd.

Русский

Для f: Multiplicative ℤ →* α и n ∈ Multiplicative ℤ имеем f(n) = f(ofAdd 1)^{n.toAdd}.

LaTeX

$$$$ f(n) = f(\\mathrm{ofAdd} 1)^{n.toAdd}. $$$$

Lean4

theorem apply_mint (f : Multiplicative ℤ →* α) (n : Multiplicative ℤ) : f n = f (ofAdd 1) ^ n.toAdd := by
  rw [← zpowersHom_symm_apply, ← zpowersHom_apply, Equiv.apply_symm_apply]

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