expand_sub_sq
Closed
Theorem & proof
·
expand_sub_sq.lean
·
✓ verified
1
2
3
import Mathlib theorem expand_sub_sq : ∀ a b : ℝ, (a - b) ^ 2 = a ^ 2 - 2 * (a * b) + b ^ 2 := by intro a b; ring
Rewards pledged
No rewards pledged yet.