comp_toFun' — Mathlib

English

For polynomial laws f : M →ₚₗ[R] N and g : N →ₚₗ[R] P, and any S with algebra, the toFun' compatibility holds: (g ∘ f).toFun' S = (g.toFun' S) ∘ (f.toFun' S).

Русский

Для полиномальных законов f и g и любого S, сохраняется совместимость toFun': (g ∘ f).toFun' S = (g.toFun' S) ∘ (f.toFun' S).

LaTeX

$$$(g.comp f).toFun'(S) = (g.toFun'(S)) \\circ (f.toFun'(S)).$$$

Lean4

theorem comp_toFun' (S : Type u) [CommSemiring S] [Algebra R S] :
    (g.comp f).toFun' S = (g.toFun' S).comp (f.toFun' S) :=
  rfl

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