OAI/Algebra/GroupRing/FramedSpherical.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TorsionFreeZeroDivisors.WordFrames.mapLabels line 15
2. def OAI.TorsionFreeZeroDivisors.WordFrames.labelCoordinates line 16
3. lemma OAI.TorsionFreeZeroDivisors.WordFrames.labelCoordinates_letter line 20
4. lemma OAI.TorsionFreeZeroDivisors.WordFrames.labelCoordinates_rotation line 29
5. lemma OAI.TorsionFreeZeroDivisors.WordFrames.cursor_map line 38
6. lemma OAI.TorsionFreeZeroDivisors.WordFrames.labelCoordinates_position line 40
7. def OAI.TorsionFreeZeroDivisors.WordFrames.spherical line 52
8. def OAI.TorsionFreeZeroDivisors.WordFrames.sphericalLift line 73
9. lemma OAI.TorsionFreeZeroDivisors.WordFrames.sphericalLift_position line 84
10. theorem OAI.TorsionFreeZeroDivisors.WordFrames.charge_zero line 94

    Source documentation

    Relator frames retain their ACTUAL conjugating coordinates when the matching is interpreted as a spherical graph picture.

    theorem charge_zero (hred : SphericalPicture.ReducesToEmpty Γ lab inv (spherical Γ d hc)) :
        (∑i : Occ (words bs),c (position (v∘lab) bs i) (letter (words bs) i))=0 := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.SphericalPicture.ReducesToEmpty, OAI.TorsionFreeZeroDivisors.WordFrames.spherical, OAI.TorsionFreeZeroDivisors.WordFrames.words, OAI.TorsionFreeZeroDivisors.WordFrames.position