OAI/Computability/QuantumFactoring/BitResidue.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.basisResidue line 13

   Source documentation

   The fixed little-endian physical representation of a modular residue.

   def basisResidue (b : ℕ) : Basis b ≃ ZMod (2^b) :=
   …

   Mentions: OAI.ExactQuantumFactoring.Basis

2. lemma OAI.ExactQuantumFactoring.finEquiv_val line 16
3. lemma OAI.ExactQuantumFactoring.basisResidue_val line 22
4. lemma OAI.ExactQuantumFactoring.basisResidue_eq line 26
5. lemma OAI.ExactQuantumFactoring.bitsValue_residue line 30
6. lemma OAI.ExactQuantumFactoring.basisResidue_bits line 34
7. lemma OAI.ExactQuantumFactoring.bitsValue_residue_add line 38
8. lemma OAI.ExactQuantumFactoring.basisResidue_zero line 46