liftAddHom_apply_single — Mathlib

English

For φ and i, applying liftAddHom to a singleton yields φ_i(x).

Русский

При применении liftAddHom к единичному элементу получается φ_i(x).

LaTeX

$$$ \\operatorname{liftAddHom} φ (\\mathrm{single } i \\; x) = φ_i(x). $$$

Lean4

/-- The `DFinsupp` version of `Finsupp.liftAddHom_apply_single` -/
theorem liftAddHom_apply_single [∀ i, AddZeroClass (β i)] [AddCommMonoid γ] (f : ∀ i, β i →+ γ) (i : ι) (x : β i) :
    liftAddHom f (single i x) = f i x := by simp

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