OAI/Algebra/GroupRing/CellNorm.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TorsionFreeZeroDivisors.CellNorm.norm line 16
2. lemma OAI.TorsionFreeZeroDivisors.CellNorm.norm_add line 17
3. lemma OAI.TorsionFreeZeroDivisors.CellNorm.norm_sub line 19
4. lemma OAI.TorsionFreeZeroDivisors.CellNorm.equivariance line 21
5. def OAI.TorsionFreeZeroDivisors.CellNorm.moduleAction line 25
6. lemma OAI.TorsionFreeZeroDivisors.CellNorm.invariant_norm line 30
7. lemma OAI.TorsionFreeZeroDivisors.CellNorm.kernel_norm line 42
8. def OAI.TorsionFreeZeroDivisors.CellNorm.augmentation line 55
9. lemma OAI.TorsionFreeZeroDivisors.CellNorm.augmentation_single line 57
10. lemma OAI.TorsionFreeZeroDivisors.CellNorm.augmentation_translate line 58
11. lemma OAI.TorsionFreeZeroDivisors.CellNorm.augmentation_norm line 63
12. lemma OAI.TorsionFreeZeroDivisors.CellNorm.augmentation_boundary line 65
13. lemma OAI.TorsionFreeZeroDivisors.CellNorm.invariant_augmentation line 72