OAI/Computability/QuantumFactoring/WordResize.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.BitArithmetic.resizeWord line 14

   Source documentation

   Ordinary zero extension/truncation, without copying a word circuit once per bit.

   def resizeWord (u w : ℕ) : BooleanNetwork u w :=
   …

   Mentions: OAI.ExactQuantumFactoring.BooleanNetwork

2. lemma OAI.ExactQuantumFactoring.BitArithmetic.resizeWord_value line 17
3. lemma OAI.ExactQuantumFactoring.BitArithmetic.resizeWord_count line 31
4. lemma OAI.ExactQuantumFactoring.BitArithmetic.resizeWord_toNat line 42