entryLinearMap_eq_comp — Mathlib

English

The identity expressing that entryAddMonoidHom equals the corresponding composition of evaluation maps with AddEquiv symmetry holds in general.

Русский

Существует тождество, выразившее равенство entryAddMonoidHom и соответствующей композиции оценочных отображений вместе с симметрией AddEquiv.

LaTeX

$$entryAddMonoidHom α i j = (((Pi.evalAddMonoidHom (fun x => α) j).comp (Pi.evalAddMonoidHom _ i)).comp (AddMonoidHomClass.toAddMonoidHom Matrix.ofAddEquiv.symm))$$

Lean4

theorem entryLinearMap_eq_comp {i : m} {j : n} :
    entryLinearMap R α i j = LinearMap.proj j ∘ₗ LinearMap.proj i ∘ₗ (ofLinearEquiv R).symm.toLinearMap := by rfl

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