Commit 2024-02-15 19:00 1e0f1e2a

View on Github →

feat: ℝ≥0 is a star-ordered ring (#10547) and other basic lemmas, including a version of Cauchy-Schwarz stated using Real.sqrt From LeanAPAP

Estimated changes

deleted theorem NNReal.le_sqrt_iff
modified theorem NNReal.mul_self_sqrt
added theorem NNReal.one_le_sqrt
modified theorem NNReal.sq_sqrt
deleted theorem NNReal.sqrt_eq_iff_sq_eq
added theorem NNReal.sqrt_eq_one
modified theorem NNReal.sqrt_eq_zero
deleted theorem NNReal.sqrt_le_iff
added theorem NNReal.sqrt_le_one
added theorem NNReal.sqrt_le_sqrt
deleted theorem NNReal.sqrt_le_sqrt_iff
added theorem NNReal.sqrt_lt_sqrt
deleted theorem NNReal.sqrt_lt_sqrt_iff
modified theorem NNReal.sqrt_mul_self
modified theorem NNReal.sqrt_one
modified theorem NNReal.sqrt_sq
modified theorem NNReal.sqrt_zero
added theorem Real.one_le_sqrt
added theorem Real.sqrt_le_one
added theorem Real.sqrt_le_sqrt_iff'
modified theorem Submonoid.mem_oneLE