OAI/LinearAlgebra/MatrixFields/Construction/GroupAssignmentRetention.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupAdmissible.Symmetries line 24
  2. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupAdmissible.rawAction line 28
  3. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupAdmissible.admissible_smul line 33
  4. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupAdmissible.admissible_of_orbitOf_eq line 71
  5. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupAdmissible.full_admissible line 94
  6. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupAdmissible.used_project_admissible line 127
  7. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupAdmissible.used_project_covered line 159
  8. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupAssignmentRetention.assigned line 190
  9. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupAssignmentRetention.physicalAssignment line 198
  10. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupAssignmentRetention.assigned_spec line 207
  11. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupAssignmentRetention.assigned_some_idealSide line 219
  12. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupCompatibility.groupIdealSide_ownWord line 252
  13. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupCompatibility.groupIdealSide_fineCompatible line 271
  14. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupCompatibility.groupIdealSide_compatible line 288
  15. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupCompatibility.admissible_compatible line 297
  16. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupAssignmentRetention.good_failure_fraction_le line 325
  17. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupAssignmentRetention.good_local_failure_le line 377
  18. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupAssignmentRetention.localAssigned_iff line 399
  19. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupAssignmentRetention.good_physical_local_failure_le line 407
  20. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupAssignmentRetention.good_projected_failure_le line 422