OAI/Analysis/GroupDeterminants/IntegralTransfer.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GroupRingDeterminant.divideGroup line 16
  2. theorem OAI.GroupRingDeterminant.kernel_integerReduction line 19
  3. def OAI.GroupRingDeterminant.toRat line 33
  4. def OAI.GroupRingDeterminant.toMod line 36
  5. theorem OAI.GroupRingDeterminant.map_toRat_zsmul line 40
  6. theorem OAI.GroupRingDeterminant.integral_transfer_of_lifts line 45
  7. theorem OAI.GroupRingDeterminant.map_toMod_zsmul line 78
  8. theorem OAI.GroupRingDeterminant.reduceGroupTwo_toMod line 84
  9. theorem OAI.GroupRingDeterminant.integer_projection_square line 92
  10. theorem OAI.GroupRingDeterminant.integral_reweight_mod_idempotent line 103
  11. theorem OAI.GroupRingDeterminant.integral_reweight_rational line 124
  12. theorem OAI.GroupRingDeterminant.integral_transfer line 137
  13. theorem OAI.GroupRingDeterminant.integral_transfer_of_congruence line 190