entryAddMonoidHom_comp_mapMatrix — Mathlib

English

The matrix-entry projection composed with the induced matrix homomorphism equals the coefficient-level projection composed with the matrix-entry.

Русский

Проекция элемента матрицы, композиция с индуцированным гомоморфизмом матриц эквивалентна композиции проекции на коэффициентах с проекцией на входную матрицу.

LaTeX

$$$\\big(\\mathrm{entryAddMonoidHom}\\ β\\ i\\ j\\big) \\circ (f.mapMatrix) = f \\circ (\\mathrm{entryAddMonoidHom}\\ α\\ i\\ j)$$$

Lean4

@[simp]
theorem entryAddMonoidHom_comp_mapMatrix (f : α →+ β) (i : m) (j : n) :
    (entryAddMonoidHom β i j).comp f.mapMatrix = f.comp (entryAddMonoidHom α i j) :=
  rfl

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