OAI/Algebra/GroupRing/ConeSigned.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TorsionFreeZeroDivisors.ConeSigned.pack line 16
2. lemma OAI.TorsionFreeZeroDivisors.ConeSigned.pack_inverse line 21
3. def OAI.TorsionFreeZeroDivisors.ConeSigned.labels line 25
4. lemma OAI.TorsionFreeZeroDivisors.ConeSigned.labels_reverse line 26
5. def OAI.TorsionFreeZeroDivisors.ConeSigned.unpack line 31
6. lemma OAI.TorsionFreeZeroDivisors.ConeSigned.reduces_to_empty line 46
7. def OAI.TorsionFreeZeroDivisors.ConeSigned.freeLetter line 56
8. lemma OAI.TorsionFreeZeroDivisors.ConeSigned.freeLetter_inverse line 57
9. lemma OAI.TorsionFreeZeroDivisors.ConeSigned.freeLetter_map line 62
10. def OAI.TorsionFreeZeroDivisors.ConeSigned.eval line 67
11. lemma OAI.TorsionFreeZeroDivisors.ConeSigned.eval_inverse line 68
12. lemma OAI.TorsionFreeZeroDivisors.ConeSigned.eval_pack line 71
13. lemma OAI.TorsionFreeZeroDivisors.ConeSigned.wordLabel_eq line 83
14. lemma OAI.TorsionFreeZeroDivisors.ConeSigned.value_mk line 89
15. lemma OAI.TorsionFreeZeroDivisors.ConeSigned.eval_value line 94