OAI/Geometry/HyperbolicGroups/PolygonCornerPrimitive.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Explicit cyclic antiderivatives for the literal threefold-subdivided polygon corners. This retains the actual constructor Position.

  1. def OAI.HyperbolicObstruction.FinitePolygonModel.Data.cornerPrimitive line 18
  2. lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.cornerPrimitive_difference line 22