OAI/Analysis/KadisonSimilarity/Tracial/MatrixTraceUniqueness.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The only tracial linear functional on a full finite matrix algebra is its value at the identity times the normalized matrix trace.

  1. theorem OAI.KadisonSimilarity.matrix_tracial_functional line 17

    Source documentation

    Matrix units determine a tracial functional, without positivity.

    theorem matrix_tracial_functional (F : Matrix ι ι ℂ →ₗ[ℂ] ℂ)
    (htr : ∀ a b, F (a * b) = F (b * a)) (a : Matrix ι ι ℂ) :
    F a = (Fintype.card ι : ℂ)⁻¹ * F 1 * Matrix.trace a := by
…