lean_workbook_plus_57227
ProvedProve that has the Archimedean property.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_57227 : ∀ x y : ℚ, x > 0 → y > 0 → ∃ n : ℕ, y < n * x := by sorry
Source
Prove that has the Archimedean property.
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_57227 : ∀ x y : ℚ, x > 0 → y > 0 → ∃ n : ℕ, y < n * x := by sorry