OAI/LinearAlgebra/MatrixFields/Extraction/ComplexRationalTypes.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.FiniteControl.every_path_safe line 15
  2. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.FiniteControl.exists_population_preserving_equiv line 30
  3. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.FiniteControl.population_product_eq line 44
  4. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.FiniteControl.exists_common_bank_multiple line 58
  5. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.FiniteControl.exists_exact_rational_tiling line 72
  6. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.FiniteControl.target_relation_of_windows line 98
  7. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.FiniteControl.synchronized_targets_of_windows line 128
  8. structure OAI.MatrixAllFields.MatrixMultiplication.Foundation.RationalLaw line 147
  9. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.RationalLaw.toFiniteLaw line 156
  10. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.RationalLaw.toFiniteLaw_mass line 161
  11. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.RationalLaw.exists_exact_counts line 164
  12. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.RationalLaw.scale_exact_counts line 181
  13. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.RationalLaw.exact_counts_zero_iff line 193
  14. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.RationalLaw.exact_counts_real_mass line 207
  15. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.RationalLaw.exists_type_representation line 217
  16. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.exists_nonnegative_rat_below line 228
  17. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.FiniteLaw.exists_rational_approximation line 250
  18. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.FiniteLaw.exists_exact_type_approximation line 334