English
If e is a bijection between κ and embeddings, then the reindexed trace matrix equals the product of reindexed embeddings matrix and its transpose, consistent with base-change formulas.
Русский
Если e — биекция между κ и вложениями, то переиндексированная матрица следа равна произведению переиндексированной матрицы вложений на её транспонированную, согласуясь с формулами смены основы.
LaTeX
$$$\\mathrm{traceMatrix}(K,b)^{\\mapsto e} = \\mathrm{embeddingsMatrixReindex}(K,E,b,e) \\cdot (\\mathrm{embeddingsMatrixReindex}(K,E,b,e))^{\\top}$$$
Lean4
theorem traceMatrix_eq_embeddingsMatrixReindex_mul_trans [Fintype κ] (e : κ ≃ (L →ₐ[K] E)) :
(traceMatrix K b).map (algebraMap K E) = embeddingsMatrixReindex K E b e * (embeddingsMatrixReindex K E b e)ᵀ := by
rw [traceMatrix_eq_embeddingsMatrix_mul_trans, embeddingsMatrixReindex, reindex_apply, transpose_submatrix, ←
submatrix_mul_transpose_submatrix, ← Equiv.coe_refl, Equiv.refl_symm]
