OAI/Analysis/Commutator/Definitions.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.commutatorSeminorm line 18

   Also declared: ComparatorChallenges/UniformCommutator.lean:12 (same declaration text).

2. def OAI.Kadison.matrixOperator line 21

   Also declared: ComparatorChallenges/UniformCommutator.lean:15 (same declaration text).

3. def OAI.Kadison.diagonalAmplification line 27

   Also declared: ComparatorChallenges/UniformCommutator.lean:21 (same declaration text).