OAI/NumberTheory/DukePrimeDegree/Geometry/RemainingProductMass.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Mass of actual remaining-root cubes under the intrinsic product

  1. lemma OAI.DukePrimeDegree.EliminationChain.remainingEuclideanCoordinates_cube line 15
  2. lemma OAI.DukePrimeDegree.EliminationChain.remainingGroup_cube_preimage line 26
  3. lemma OAI.DukePrimeDegree.EliminationChain.remainingProduct_cube_mass line 56
  4. theorem OAI.DukePrimeDegree.EliminationChain.ae_remainingIntrinsicProduct_unit line 66