OAI/Analysis/KadisonSimilarity/Similarity/SimilarityRetract.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Similarity descends to a bounded algebraic retract. This is used for the first-coordinate corner after finite matrix amplification.

  1. theorem OAI.KadisonSimilarity.similarity_of_retract line 17