OAI/Analysis/GroupDeterminants/TransferTrace.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GroupRingDeterminant.topBlockIdentity line 12
2. def OAI.GroupRingDeterminant.bottomBlock line 15
3. def OAI.GroupRingDeterminant.lowerNil line 18
4. def OAI.GroupRingDeterminant.upperNil line 21
5. lemma OAI.GroupRingDeterminant.lowerNil_square line 24
6. lemma OAI.GroupRingDeterminant.upperNil_square line 26
7. lemma OAI.GroupRingDeterminant.lowerShear_eq_one_add line 29
8. lemma OAI.GroupRingDeterminant.upperShear_eq_one_add line 34
9. lemma OAI.GroupRingDeterminant.transfer_diagonal_weightedPair line 39
10. lemma OAI.GroupRingDeterminant.transfer_trace_log line 53