pith. machine review for the scientific record. sign in
theorem proved tactic proof

two_pi_not_D3

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 126theorem two_pi_not_D3 : 2 * Real.pi ≠ 4 * Real.pi := by

proof body

Tactic-mode proof.

 127  intro h
 128  have hpi_ne : Real.pi ≠ 0 := ne_of_gt Real.pi_pos
 129  have : (2 : ℝ) = 4 := by
 130    have := mul_right_cancel₀ hpi_ne h
 131    linarith
 132  norm_num at this
 133
 134/-- 8π is the surface of a sphere with radius √2, not the unit sphere. -/

depends on (10)

Lean names referenced from this declaration's body.