traceMatrix_eq_embeddingsMatrix_mul_trans

English

When changing the base up to an embedding substitution, the base-changed trace matrix equals the product of the reindexed embeddings matrix with its transpose.

Русский

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

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_embeddingsMatrix_mul_trans :
    (traceMatrix K b).map (algebraMap K E) = embeddingsMatrix K E b * (embeddingsMatrix K E b)ᵀ := by ext (i j);
  simp [trace_eq_sum_embeddings, embeddingsMatrix, Matrix.mul_apply]

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