OAI/Analysis/FreeWords/FlipAverage.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KKFreeLiftDiagnostic.leftAverage line 14
2. theorem OAI.KKFreeLiftDiagnostic.left_single_mul line 18
3. theorem OAI.KKFreeLiftDiagnostic.mul_left_single line 28
4. theorem OAI.KKFreeLiftDiagnostic.leftAverage_eq_partialTrace line 38
5. theorem OAI.KKFreeLiftDiagnostic.leftAverage_centeredFlip line 48