lean_workbook_plus_7615
Proved.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_7615 (x y k : ℝ) (h₀ : x + 1/y = k) (h₁ : y ≠ 0) (h₂ : k*y - 1 ≠ 0) : x = (k*y - 1)/y ∧ 1/x = y/(k*y - 1) := by sorry
Source
.
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_7615 (x y k : ℝ) (h₀ : x + 1/y = k) (h₁ : y ≠ 0) (h₂ : k*y - 1 ≠ 0) : x = (k*y - 1)/y ∧ 1/x = y/(k*y - 1) := by sorry