lean_workbook_plus_2544
ProvedDoesn't simplify to ?
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_2544 (s : ℝ) (h : s ≠ 0) : 6 * s ^ 2 / (2 * s ^ 2 * Real.sqrt 3) = 3 / Real.sqrt 3 := by sorry
Source
Doesn't simplify to ?
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_2544 (s : ℝ) (h : s ≠ 0) : 6 * s ^ 2 / (2 * s ^ 2 * Real.sqrt 3) = 3 / Real.sqrt 3 := by sorry