map_dfinsuppSumAddHom — Mathlib

English

Under a linear equivalence, the sumAddHom construction commutes with f.

Русский

При линейном эквиваленте суммационные конструции сохраняются через f.

LaTeX

$$f (sumAddHom g t) = sumAddHom (fun i => f.toAddEquiv.toAddMonoidHom.comp (g i)) t$$

Lean4

@[simp]
theorem map_dfinsuppSumAddHom [∀ i, AddZeroClass (γ i)] (f : M ≃ₛₗ[τ₁₂] M₂) (t : Π₀ i, γ i) (g : ∀ i, γ i →+ M) :
    f (sumAddHom g t) = sumAddHom (fun i => f.toAddEquiv.toAddMonoidHom.comp (g i)) t :=
  f.toAddEquiv.map_dfinsuppSumAddHom _ _

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