compMulHom — Mathlib

English

Composition with a cocompact map is a multiplicative homomorphism: (f1 · f2) ∘ g = (f1 ∘ g) · (f2 ∘ g).

Русский

Композиция с кокопактом сохраняет умножение: (f1 · f2) ∘ g = (f1 ∘ g) · (f2 ∘ g).

LaTeX

$$(f1 \cdot f2) \circ g = (f1 \circ g) \cdot (f2 \circ g)$$

Lean4

/-- Composition as a semigroup homomorphism. -/
def compMulHom [MulZeroClass δ] [ContinuousMul δ] (g : β →co γ) : C₀(γ, δ) →ₙ* C₀(β, δ)
    where
  toFun f := f.comp g
  map_mul' _ _ := rfl

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