Pythagorass_Theorem

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

proofwikipythagoras-s-theoremright-triangles

Let triangle ABC be a right triangle with c as the hypotenuse. Then a^2 + b^2 = c^2

Preamble

import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Tactic

Formal statement

theorem Pythagorass_Theorem (a b c : ℝ) (h : a ^ 2 + b ^ 2 = c ^ 2) : c ^ 2 = a ^ 2 + b ^ 2 := by sorry

Source