entryAddHom_comp_mapMatrix — Mathlib

English

For an additive equivalence f, the matrix-entry homomorphism composed with the induced matrix homomorphism equals the coefficient-level homomorphism composed with the entry-homomorphism.

Русский

Для аддитивного эквивалентного f композиция матричной проекции и индуцированного гомоморфизма матриц равна композиции гомоморфизма коэффициентов с проекцией на элемент матрицы.

LaTeX

$$$\\big(\\mathrm{entryAddHom}\\ β i j\\big) \\circ (AddHomClass.toAddHom f.mapMatrix) = (f : AddHom α β) \\circ (\\mathrm{entryAddHom}\\ _\\ i\\ j)$$$

Lean4

@[simp]
theorem entryAddHom_comp_mapMatrix (f : α ≃+ β) (i : m) (j : n) :
    (entryAddHom β i j).comp (AddHomClass.toAddHom f.mapMatrix) = (f : AddHom α β).comp (entryAddHom _ i j) :=
  rfl

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