OAI/NumberTheory/DukePrimeDegree/Geometry/RemainingIntrinsicProduct.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The intrinsic root product on each remaining subgroup

Its coordinates are actual matrix entries, so the measure is independent of the Gaussian elimination chain used to define the coordinate chart.

  1. def OAI.DukePrimeDegree.EliminationChain.remainingIntrinsicProduct line 19
  2. lemma OAI.DukePrimeDegree.EliminationChain.remainingGroupCoordinates_eq line 27
  3. lemma OAI.DukePrimeDegree.EliminationChain.remainingIntrinsicProduct_chain_independent line 36
  4. lemma OAI.DukePrimeDegree.EliminationChain.remainingIntrinsicProduct_done line 44
  5. theorem OAI.DukePrimeDegree.EliminationChain.ae_remainingIntrinsicProduct_locallyFinite line 55