embeddingsMatrixReindex_eq_vandermonde

English

Under a power basis, reindexing the embeddings matrix yields the transpose of a Vandermonde matrix built from the images of the power-basis generator under the embeddings.

Русский

При мощности базиса переиндексация матрицы вложений даёт транспонированную матрицу Вандермонде, составленную из образов генератора базиса под вложениями.

LaTeX

$$$\\mathrm{embeddingsMatrixReindex}(A,C,\\text{pb.basis},e) = \\big( \\mathrm{vandermonde}(i \\mapsto e(i)\\,\\text{pb.gen}) \\big)^{\\top}$$$

Lean4

theorem embeddingsMatrixReindex_eq_vandermonde (pb : PowerBasis A B) (e : Fin pb.dim ≃ (B →ₐ[A] C)) :
    embeddingsMatrixReindex A C pb.basis e = (vandermonde fun i => e i pb.gen)ᵀ :=
  by
  ext i j
  simp [embeddingsMatrixReindex, embeddingsMatrix]

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