entryAddHom — Mathlib

English

For i ∈ m, j ∈ n, the (i,j) entry extraction map equals the composition of Pi.evalAddHom maps along i and j with the canonical AddEquiv identification.

Русский

Для i ∈ m, j ∈ n отображение извлечения элемента (i,j) равняется композиции Pi.evalAddHom по i и j с каноническим соответствием AddEquiv.

LaTeX

$$entryAddHom α i j = ((Pi.evalAddHom (fun _ => α) j).comp (Pi.evalAddHom _ i)).comp (AddHomClass.toAddHom ofAddEquiv.symm)$$

Lean4

/-- Extracting entries from a matrix as an additive homomorphism. -/
@[simps]
def entryAddHom (i : m) (j : n) : AddHom (Matrix m n α) α
    where
  toFun M := M i j
  map_add' _ _ := rfl

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