pith. machine review for the scientific record. sign in
structure definition def or abbrev

SubsetProductPhaseHit

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)

  29structure SubsetProductPhaseHit (n c : ℕ) where
  30  x : ℕ
  31  N : ℕ
  32  box : DivisorExponentBox N
  33  n_pos : 0 < n
  34  c_pos : 0 < c
  35  x_pos : 0 < x
  36  N_pos : 0 < N
  37  N_eq : N = n * x
  38  c_eq : c = 4 * x - n
  39  divisor_phase : c ∣ N + boxDivisor box
  40  complement_phase : c ∣ N + boxComplement box
  41
  42/-- The target phase in the residual quotient. -/

used by (11)

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

depends on (8)

Lean names referenced from this declaration's body.