Pythagorean theorem
Closed
Theorem & proof
·
pythag_thm.lean
·
✓ verified
1
2
3
4
5
6
7
import Mathlib theorem pythag_thm (a b c : ℝ) (h : c = Real.sqrt (a ^ 2 + b ^ 2)) : a ^ 2 + b ^ 2 = c ^ 2 := by rw [h] symm apply Real.sq_sqrt positivity
Rewards pledged
No rewards pledged yet.