entryAddHom_eq_comp — Mathlib

English

Similarly to AddHom, the (i,j) entry extraction as an AddMonoidHom equals the corresponding composition of Pi.evalAddMonoidHom maps with the canonical symmetry.

Русский

Точно так же, как и ранее, отображение извлечения элемента (i,j) как AddMonoidHom равняется соответствующей композиции Pi.evalAddMonoidHom с симметрией.

LaTeX

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

Lean4

theorem entryAddHom_eq_comp {i : m} {j : n} :
    entryAddHom α i j =
      ((Pi.evalAddHom (fun _ => α) j).comp (Pi.evalAddHom _ i)).comp (AddHomClass.toAddHom ofAddEquiv.symm) :=
  rfl

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