vec_bijective — Mathlib

English

The map vec from square matrices to vectors is a bijection; it has an inverse and is both injective and surjective.

Русский

Отображение vec между квадратными матрицами и векторами является биекцией; существует обратное отображение.

LaTeX

$$$$\operatorname{vec}: \mathrm{Mat}_{m\times n}(R) \to R^{mn} \quad \text{is bijective}$$$$

Lean4

theorem vec_bijective : Function.Bijective (vec : Matrix m n R → _) :=
  Equiv.curry _ _ _ |>.symm.bijective.comp Function.swap_bijective

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