sq_nonneg_real
Closed
Theorem & proof
·
sq_nonneg_real.lean
·
✓ verified
1
2
3
import Mathlib theorem sq_nonneg_real : ∀ x : ℝ, 0 ≤ x ^ 2 := fun x => sq_nonneg x
Rewards pledged
No rewards pledged yet.