pith. machine review for the scientific record. sign in
theorem proved term proof

box_divisor_mul_complement

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  39theorem box_divisor_mul_complement {N : ℕ} (box : DivisorExponentBox N) :
  40    boxDivisor box * boxComplement box = N ^ 2 :=

proof body

Term-mode proof.

  41  box.square_budget
  42
  43/-- A square-budget box hits the balanced residual phase for gate `c`.
  44
  45The conditions `c | N+d` and `c | N+e` say exactly that both reciprocal
  46defects land in phase `-N` modulo `c`. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (14)

Lean names referenced from this declaration's body.