lean_workbook_plus_69480
ProvedFor the first question, we have .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_69480 (n : ℝ) (hn : n ≠ 0) : ((n + 2) / (6 * n) : ℝ) = 1 / 5 ↔ n = 10 := by sorry
Source
For the first question, we have .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_69480 (n : ℝ) (hn : n ≠ 0) : ((n + 2) / (6 * n) : ℝ) = 1 / 5 ↔ n = 10 := by sorry