English
For any integral element α, the inverse of the transpose of the basis matrix, applied to the canonical embeddings vector of α, yields the coordinate representation of α in the integral basis.
Русский
Для целочисленного элемента α, произведение обратной транспонированной базисной матрицы на вектор канонических вложений дает координаты α в интегральной базе.
LaTeX
$$$$ (\\text{basisMatrix}(K)^{T})^{-1} \\cdot \\operatorname{mulVec}( \\text{canonicalEmbedding}(K) , \\alpha ) = \\text{repr}_{\\mathcal{O}_K}(\\alpha). $$$$
Lean4
theorem inverse_basisMatrix_mulVec_eq_repr [DecidableEq (K →+* ℂ)] (α : 𝓞 K) :
∀ i,
((basisMatrix K).transpose)⁻¹.mulVec (fun j => canonicalEmbedding K (algebraMap (𝓞 K) K α) j) i =
((integralBasis K).reindex (equivReindex K).symm).repr α i :=
fun i => by rw [inv_mulVec_eq_vec (canonicalEmbedding_eq_basisMatrix_mulVec ((algebraMap (𝓞 K) K) α))]
