ofAddEquiv — Mathlib

English

There is an additive equivalence between the space of functions m → n → α and the space of matrices m × n with entries α, given by f ↦ of f.

Русский

Существует аддитивное эквивалентие между пространством функций m → n → α и пространством матриц m × n над α, задаваемое f ↦ of f.

LaTeX

$$$ (m \\to n \\to \\alpha) \\simeq_{+} \\mathrm{Matrix}(m,n,\\alpha) $$$

Lean4

/-- This is `Matrix.of` bundled as an additive equivalence. -/
def ofAddEquiv [Add α] : (m → n → α) ≃+ Matrix m n α
    where
  __ := of
  map_add' _ _ := rfl

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