OAI/Analysis/Commutator/FinitePairings3.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Kadison.TailSlots line 23
2. lemma OAI.Kadison.finite_constant_coefficient_bound line 25
3. lemma OAI.Kadison.finite_pairing_source_bound line 40
4. lemma OAI.Kadison.finite_pairing_test_bound line 86