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

computable_div

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)

 230theorem computable_div {x y : ℝ} (hx : Computable x) (hy : Computable y) (hne : y ≠ 0) :
 231    Computable (x / y) := by

proof body

Term-mode proof.

 232  -- Immediate from the global classical instance.
 233  infer_instance
 234
 235/-- Computable reals are closed under natural number exponentiation.
 236    Proof by induction: x^0 = 1 (computable), x^(n+1) = x * x^n (by computable_mul). -/

used by (1)

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

depends on (3)

Lean names referenced from this declaration's body.