Theorem InnerProductSpace.trace_rankOne

Modification history

2026-01-06 18:26

Mathlib/Analysis/InnerProductSpace/Trace.lean

feat(Analysis/InnerProductSpace): define rank-one operators (#33439) …

Added InnerProductSpace.trace_rankOne View on Github →