Theorem NNReal.sqrt_eq_iff_eq_sq

Modification history

2026-08-06 00:34
Mathlib/Analysis/Real/Sqrt.lean
chore: deprecate apply_eq_iff_eq_symm_apply (#42094) …
Modified NNReal.sqrt_eq_iff_eq_sqView on Github →
2024-02-15 19:00
Mathlib/Data/Real/Sqrt.lean
feat: `ℝ≥0` is a star-ordered ring (#10547) …
Added NNReal.sqrt_eq_iff_eq_sqView on Github →