compAddMonoidHom — Mathlib

English

Composition with g defines an additive monoid homomorphism from C_c(γ, δ) to C_c(β, δ): (f + f') ∘ g = f ∘ g + f' ∘ g and 0 ∘ g = 0.

Русский

Композиция с g задаёт аддитивный моноид-гомоморфизм: (f + f') ∘ g = f ∘ g + f' ∘ g и 0 ∘ g = 0.

LaTeX

$$$$ (f + f') \circ g = f \circ g + f' \circ g, \quad 0 \circ g = 0. $$$$

Lean4

/-- Composition as an additive monoid homomorphism. -/
def compAddMonoidHom [AddMonoid δ] [ContinuousAdd δ] (g : β →co γ) : C_c(γ, δ) →+ C_c(β, δ)
    where
  toFun f := f.comp g
  map_zero' := zero_comp g
  map_add' _ _ := rfl

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