OAI/Analysis/GroupDeterminants/ModularLifting.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GroupRingDeterminant.reduceTwo line 15
  2. theorem OAI.GroupRingDeterminant.kernel_reduceTwo line 18
  3. def OAI.GroupRingDeterminant.reduceGroupTwo line 32
  4. def OAI.GroupRingDeterminant.halfGroup line 35
  5. theorem OAI.GroupRingDeterminant.kernel_reduceGroupTwo line 40
  6. theorem OAI.GroupRingDeterminant.twice_pow_eq_zero line 50
  7. theorem OAI.GroupRingDeterminant.matrix_kernel_nilpotent line 61
  8. theorem OAI.GroupRingDeterminant.reduceGroupTwo_surjective line 75
  9. theorem OAI.GroupRingDeterminant.integerReduction_surjective line 79
  10. theorem OAI.GroupRingDeterminant.lift_binary_factorization line 88
  11. theorem OAI.GroupRingDeterminant.exists_binary_modulus line 114