OAI/NumberTheory/DukePrimeDegree/Geometry/RemainingGroupCenter.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Centered Gaussian coordinates with values in the actual subgroup

  1. def OAI.DukePrimeDegree.EliminationChain.remainingGroupCenter line 14
  2. lemma OAI.DukePrimeDegree.EliminationChain.remainingGroupCenter_image line 20
  3. lemma OAI.DukePrimeDegree.EliminationChain.remainingGroupCenter_map line 28
  4. lemma OAI.DukePrimeDegree.EliminationChain.basedRemainingGroupMeasure_eq_smul_center line 38