OAI/Algebra/GroupRing/ConeArea.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TorsionFreeZeroDivisors.ConeArea.letters_reverse line 21
2. lemma OAI.TorsionFreeZeroDivisors.ConeArea.path_value line 23
3. lemma OAI.TorsionFreeZeroDivisors.ConeArea.root_value line 31
4. lemma OAI.TorsionFreeZeroDivisors.ConeArea.root_charge line 34
5. lemma OAI.TorsionFreeZeroDivisors.ConeArea.eval_reverse line 41
6. lemma OAI.TorsionFreeZeroDivisors.ConeArea.charge_reverse line 46
7. lemma OAI.TorsionFreeZeroDivisors.ConeArea.reverse_root_charge line 52
8. lemma OAI.TorsionFreeZeroDivisors.ConeArea.triangle_charge line 60
9. def OAI.TorsionFreeZeroDivisors.ConeArea.loops line 68
10. def OAI.TorsionFreeZeroDivisors.ConeArea.words line 70
11. lemma OAI.TorsionFreeZeroDivisors.ConeArea.words_mk line 73
12. lemma OAI.TorsionFreeZeroDivisors.ConeArea.loop_value line 80
13. lemma OAI.TorsionFreeZeroDivisors.ConeArea.loop_charge line 86
14. lemma OAI.TorsionFreeZeroDivisors.ConeArea.signed_charge line 96
15. lemma OAI.TorsionFreeZeroDivisors.ConeArea.term_value line 109
16. def OAI.TorsionFreeZeroDivisors.ConeArea.termArea line 123
17. lemma OAI.TorsionFreeZeroDivisors.ConeArea.termArea_eq line 128
18. theorem OAI.TorsionFreeZeroDivisors.ConeArea.identity_zero line 136

    Source documentation

    Every actual free identity of the physical triangular presentation has zero integral translated physical-cell area. No cellular realization is presumed.

    theorem identity_zero
        (hex : ∀{P : Type}[Fintype P][Nonempty P]
          (a : SphericalPicture.Data (O:=P) Γ label WordPairing.inverseLetter),¬a.Reduced)
    …

    Mentions: OAI.TorsionFreeZeroDivisors.SphericalPicture.Data, OAI.TorsionFreeZeroDivisors.WordPairing.inverseLetter