coe_comp_monoidWithZeroHom — Mathlib

English

Under the composition, the coercion to a monoid with zero homomorphism matches the corresponding composition on monoidWithZeroHom.

Русский

При композиции приведение к MonoidWithZeroHom соответствует композиции на MonoidWithZeroHom.

LaTeX

$$$ (f.comp g) = (f : β \to_*_0 γ) \circ (g : α \to_*_0 β) $$$

Lean4

theorem coe_comp_monoidWithZeroHom (f : β →*₀o γ) (g : α →*₀o β) : (f.comp g : α →*₀ γ) = (f : β →*₀ γ).comp g :=
  rfl

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