OAI/Analysis/GroupDeterminants/ClosedTrace.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GroupRingDeterminant.subTrace line 18
2. lemma OAI.GroupRingDeterminant.subTrace_apply line 21
3. lemma OAI.GroupRingDeterminant.subalgebra_log_coe line 23
4. lemma OAI.GroupRingDeterminant.subTrace_mul_comm line 30
5. lemma OAI.GroupRingDeterminant.subTrace_star line 34
6. lemma OAI.GroupRingDeterminant.trace_log_shear_invariant_subalgebra line 37
7. instance OAI.GroupRingDeterminant.closedGroupAlgebra_isClosed line 68
8. def OAI.GroupRingDeterminant.closedRepresentation line 72
9. theorem OAI.GroupRingDeterminant.closedRepresentation_coe line 77
10. theorem OAI.GroupRingDeterminant.groupTrace_log_shear_invariant line 80