coeff_comp — Mathlib

English

For g in Lex(Prod Γ' Γ), the coefficient of comp A B at g equals A.coeff (ofLex g).2 composed with B.coeff (ofLex g).1.

Русский

Для g ∈ Lex(Prod Γ' Γ) коэффициент (comp A B) в g равен A.coeff( ofLex g ).2 ∘ B.coeff (ofLex g).1.

LaTeX

$$$(\mathrm{comp}\ A\ B).\mathrm{coeff}\ g = A.\mathrm{coeff}((\mathrm{ofLex}\ g).2) \circ_\ell B.\mathrm{coeff}((\mathrm{ofLex}\ g).1)$$$

Lean4

@[simp]
theorem coeff_comp (g : Γ' ×ₗ Γ) : (comp A B).coeff g = A.coeff (ofLex g).2 ∘ₗ B.coeff (ofLex g).1 := by rfl

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