OAI/Computability/QuantumFactoring/PrimePowerLevels.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.primePowerUnitCount line 16

   Source documentation

   A closed integer expression; no enumeration of residue classes.

   def primePowerUnitCount (p e : ℕ) : ℕ := (p-1) * p^(e-1)

2. def OAI.ExactQuantumFactoring.closedLevelCount line 18
3. def OAI.ExactQuantumFactoring.primePowerLevelCard line 22
4. theorem OAI.ExactQuantumFactoring.primePowerLevelCard_eq line 27

   Source documentation

   Exact prime-power level counts from the already fully proved cyclicity of odd prime-power unit groups in Mathlib.

   theorem primePowerLevelCard_eq {p e : ℕ} (hp : p.Prime) (hp2 : p ≠ 2)
       (he : 0 < e) (t : ℕ) :
       primePowerLevelCard p e t = closedLevelCount (primePowerUnitCount p e) t := by
   …

   Mentions: OAI.ExactQuantumFactoring.primePowerLevelCard, OAI.ExactQuantumFactoring.closedLevelCount, OAI.ExactQuantumFactoring.primePowerUnitCount

5. theorem OAI.ExactQuantumFactoring.primePowerLevelCard_half line 42