traceAux_eq — Mathlib

English

The traceAux map is independent of the chosen basis: traceAux R b = traceAux R c for any bases b, c of M.

Русский

Следопределение не зависит от выбора базиса: traceAux R b = traceAux R c для любых базисов b и c в M.

LaTeX

$$$\\text{traceAux}_R(b) = \\text{traceAux}_R(c)$$$

Lean4

theorem traceAux_eq : traceAux R b = traceAux R c :=
  LinearMap.ext fun f =>
    calc
      Matrix.trace (LinearMap.toMatrix b b f) =
          Matrix.trace (LinearMap.toMatrix b b ((LinearMap.id.comp f).comp LinearMap.id)) :=
        by rw [LinearMap.id_comp, LinearMap.comp_id]
      _ =
          Matrix.trace
            (LinearMap.toMatrix c b LinearMap.id * LinearMap.toMatrix c c f * LinearMap.toMatrix b c LinearMap.id) :=
        by rw [LinearMap.toMatrix_comp _ c, LinearMap.toMatrix_comp _ c]
      _ =
          Matrix.trace
            (LinearMap.toMatrix c c f * LinearMap.toMatrix b c LinearMap.id * LinearMap.toMatrix c b LinearMap.id) :=
        by rw [Matrix.mul_assoc, Matrix.trace_mul_comm]
      _ = Matrix.trace (LinearMap.toMatrix c c ((f.comp LinearMap.id).comp LinearMap.id)) := by
        rw [LinearMap.toMatrix_comp _ b, LinearMap.toMatrix_comp _ c]
      _ = Matrix.trace (LinearMap.toMatrix c c f) := by rw [LinearMap.comp_id, LinearMap.comp_id]

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