English
The basis matrix for the embeddings of K into ℂ is obtained by taking the lattice basis vectors of K, reindexing them via the equivReindex correspondence, and transposing the resulting matrix.
Русский
Базисная матрица для вложений K в ℂ получается из базиса решетки K, перестановки индексов через соответствие equivReindex и транспонирования полученной матрицы.
LaTeX
$$$$\\text{basisMatrix}(K) = \\big(\\text{latticeBasis}(K,\\text{equivReindex}(K))\\big)^{T}.$$$$
Lean4
/-- The basis matrix for the embeddings of `K` into `ℂ`. This matrix is formed by
taking the lattice basis vectors of `K` and reindexing them according to the
equivalence `equivReindex`, then transposing the resulting matrix. -/
abbrev basisMatrix : Matrix (K →+* ℂ) (K →+* ℂ) ℂ :=
(Matrix.of fun i ↦ latticeBasis K (equivReindex K i))
