rename_psum — Mathlib

English

For a bijection e: σ ≃ τ, rename e preserves psum: rename e (psum(σ,R,n)) = psum(τ,R,n).

Русский

При биекции e: σ ≃ τ сумма psum сохраняется: rename e (psum(σ,R,n)) = psum(τ,R,n).

LaTeX

$$$\\operatorname{rename}_{e}(\\mathrm{psum}_{\\sigma,R}(n)) = \\mathrm{psum}_{\\tau,R}(n)$$$

Lean4

@[simp]
theorem rename_psum (n : ℕ) (e : σ ≃ τ) : rename e (psum σ R n) = psum τ R n := by
  simp_rw [psum, map_sum, map_pow, rename_X, e.sum_comp (X · ^ n)]

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