OAI/Analysis/GroupDeterminants/Defects.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GroupRingDeterminant.CompanionInput line 12
  2. theorem OAI.GroupRingDeterminant.no_finite_group_input line 17
  3. theorem OAI.GroupRingDeterminant.regularOperator_unique line 25
  4. theorem OAI.GroupRingDeterminant.fkDet_pos line 32
  5. theorem OAI.GroupRingDeterminant.defect_idempotent line 39
  6. theorem OAI.GroupRingDeterminant.mul_defect line 50
  7. theorem OAI.GroupRingDeterminant.defect_mul line 53
  8. theorem OAI.GroupRingDeterminant.defect_ne_zero line 56
  9. theorem OAI.GroupRingDeterminant.defect_factorization line 64
  10. def OAI.GroupRingDeterminant.cornerSeries line 79
  11. theorem OAI.GroupRingDeterminant.cornerSeries_spec line 82
  12. theorem OAI.GroupRingDeterminant.lift_rectangular_factorization line 110