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

has_prime_factor

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)

 113theorem has_prime_factor (n : ℕ) (hn : 1 < n) :
 114    ∃ p : ℕ, Nat.Prime p ∧ p ∣ n :=

proof body

Term-mode proof.

 115  Nat.exists_prime_and_dvd (by omega)
 116
 117/-! ## J-Cost on the Multiplicative Ledger
 118
 119Each ratio in the ledger carries J-cost. The total cost of a
 120transaction n is related to the costs of its prime factors
 121through the d'Alembert identity (the RCL). -/
 122
 123/-- The d'Alembert identity for J-cost:
 124    J(xy) + J(x/y) = 2J(x) + 2J(y) + 2J(x)J(y) -/

depends on (18)

Lean names referenced from this declaration's body.