OAI/RingTheory/BassTrace/FiniteGenerators.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BassTrace.trace_coeff line 18
2. lemma OAI.BassTrace.classCoefficient_eq_finsum line 22
3. lemma OAI.BassTrace.totalWeight_eq_classCoefficient line 33
4. lemma OAI.BassTrace.sum_conjugacy_invariant_zero line 39
5. lemma OAI.BassTrace.exists_symmetric_generators line 72
6. def OAI.BassTrace.restrictMatrix line 91
7. lemma OAI.BassTrace.restrictMatrix_map line 95
8. lemma OAI.BassTrace.restrictMatrix_idempotent line 104
9. lemma OAI.BassTrace.map_trace_restrict line 116
10. lemma OAI.BassTrace.classCoefficient_map_subgroup line 124