OAI/Geometry/HyperbolicGroups/StepChain.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.PictureSwitch.sum_offPair line 18

   Source documentation

   Common-side cancellation and backtrack removal retain the EXACT sum of oriented elementary cone triangles, with arbitrary additive coefficients.

   lemma sum_offPair {a b : D} (hab : a ≠ b) (q : D → A) (hq : q a + q b = 0) :
       ∑ x : {x // OffPair a b x}, q x.val = ∑ x : D, q x := by
   …

   Mentions: OAI.HyperbolicObstruction.PictureSwitch.OffPair