OAI/LinearAlgebra/MatrixFields/Parameters/PopulationCounts.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldPopulationCounts.denominator line 18
  2. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldPopulationCounts.baseCount line 20
  3. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldPopulationCounts.count line 23
  4. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldPopulationCounts.blockLength line 25
  5. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldPopulationCounts.denominator_pos line 28
  6. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldPopulationCounts.denominator_factor line 31
  7. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldPopulationCounts.baseCount_cast line 35
  8. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldPopulationCounts.count_cast line 51
  9. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldPopulationCounts.count_cast_blockLength line 55
  10. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldPopulationCounts.blockLength_pos line 61
  11. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldPopulationCounts.count_zero_iff line 64
  12. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldPopulationCounts.count_pos_iff line 74
  13. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldPopulationCounts.sum_count_cast line 82
  14. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldPopulationCounts.transition_sum line 89
  15. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldPopulationCounts.unit_sum line 96
  16. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldPopulationCounts.count_eq_of_mass_eq line 103
  17. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldPopulationCounts.count_ratio line 108
  18. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldPopulationCounts.count_dilate line 116
  19. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldPopulationCounts.dilation_le_count line 119
  20. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldPopulationCounts.two_le_positive_count line 128