OAI/Analysis/Commutator/PairingElimination.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Kadison.pairing_coefficient_zero_source line 68
2. theorem OAI.Kadison.pairing_coefficient_zero_test line 115
3. theorem OAI.Kadison.pairing_crossing_card_eq line 156
4. theorem OAI.Kadison.pairing_coefficients_zero_of_ne line 177