lean_workbook_plus_1843
Provedsqrt(1043*3) (Heron's formula) ->
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_1843 (a : ℝ) (h : a = 10) : Real.sqrt (10 * 4 * 3 * 3) = 6 * Real.sqrt 10 := by sorry
Source
sqrt(1043*3) (Heron's formula) ->
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_1843 (a : ℝ) (h : a = 10) : Real.sqrt (10 * 4 * 3 * 3) = 6 * Real.sqrt 10 := by sorry