OAI/NumberTheory/DukePrimeDegree/Geometry/RootPrefixIntrinsicCandidates.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

From intrinsic long-box leaves to an actual regional conditional kernel

  1. theorem OAI.DukePrimeDegree.RootPrefixCoordinates.timeParam_injective_of_free_at_coordinate line 20
  2. theorem OAI.DukePrimeDegree.RootPrefixCoordinates.ae_region_kernel_of_intrinsic_boxes line 31