Trace of diagonal

Stream: Is there code for X?

[Damiano Testa]

Dear All,

does Mathlib already contain a lemma similar to the one below?

import Mathlib.LinearAlgebra.Matrix.Trace

lemma Matrix.trace_diagonal {R o} [AddCommMonoid R] [Fintype o] [DecidableEq o] (d : o → R) :
    Matrix.trace (Matrix.diagonal d) = (Finset.univ : Finset o).sum d := by
  sorry

Thanks!

[Kevin Buzzard]

import Mathlib.LinearAlgebra.Matrix.Trace

lemma Matrix.trace_diagonal {R o} [AddCommMonoid R] [Fintype o] [DecidableEq o] (d : o → R) :
    Matrix.trace (Matrix.diagonal d) = (Finset.univ : Finset o).sum d := by
  simp [Matrix.trace]

[Eric Wieser]

I think it's also true by rfl?

[Kevin Buzzard]

yeah I tried that first :-)

[Kevin Buzzard]

docs#Matrix.diagonal_apply_eq isn't rfl apparently

[Kevin Buzzard]

diagonal has an if in its definition.

[Damiano Testa]

:face_palm: I did not think of unfolding!

[Damiano Testa]

Thanks!

[Damiano Testa]

Do you agree that this lemma should be in mathlib?

[Kevin Buzzard]

yeah I couldn't find it and the name is pretty obvious

[Damiano Testa]

#7061