lean_workbook_plus_39229
ProvedApplied it here: , so
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_39229 (x_A y_A : ℝ) (h : x_A > 0 ∧ y_A > 0) : (x_A / y_A = 1 ↔ x_A = y_A) := by sorry
Source
Applied it here: , so
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_39229 (x_A y_A : ℝ) (h : x_A > 0 ∧ y_A > 0) : (x_A / y_A = 1 ↔ x_A = y_A) := by sorry