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

generated_phase_hit_gives_HitsBalancedPhase

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)

  56theorem generated_phase_hit_gives_HitsBalancedPhase {n c : ℕ}
  57    (hit : SubsetProductPhaseHit n c) :
  58    HitsBalancedPhase n c := by

proof body

Term-mode proof.

  59  refine ⟨hit.x, hit.N, hit.box,
  60    hit.n_pos, hit.c_pos, hit.x_pos, hit.N_pos,
  61    hit.N_eq, hit.c_eq, hit.divisor_phase, hit.complement_phase⟩
  62
  63/-- Hence a generated target phase gives the rational Erdős-Straus
  64representation. -/

used by (3)

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

depends on (7)

Lean names referenced from this declaration's body.