OAI/LinearAlgebra/MatrixFields/Histories/ZeroHistorySums.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroHistorySums.zeroRate line 21
2. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroHistorySums.subtype_sum_indicator_inline_MatrixMultiplication_AllFieldZeroHistorySums line 25
3. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroHistorySums.sum_subtype_complement line 31
4. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroHistorySums.list_filter_sum_inline_MatrixMultiplication_AllFieldZeroHistorySums line 41
5. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroHistorySums.sum_placement_rate line 48
6. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroHistorySums.a_zero_canonical_rate line 63
7. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroHistorySums.a_zero_history_rate line 86
8. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroHistorySums.b_positive_secondLeafRate line 97
9. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroHistorySums.b_zero_canonical_rate line 110
10. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroHistorySums.b_zero_rate_eq_secondLeafRate line 119
11. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroHistorySums.b_zero_history_rate line 125
12. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroHistorySums.zero_history_sum line 140