chore: fix 2 comments (#4346)

leanprover-community · May 25, 2023 · 18ecd67 · 18ecd67
1 parent 73ad900
commit 18ecd67
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/Mathlib/Data/Real/ENNReal.lean b/Mathlib/Data/Real/ENNReal.lean
@@ -1640,12 +1640,12 @@ theorem mul_le_iff_le_inv {a b r : ℝ≥0∞} (hr₀ : r ≠ 0) (hr₁ : r ≠
     one_mul]
 #align ennreal.mul_le_iff_le_inv ENNReal.mul_le_iff_le_inv
 
-/-- A variant of `le_inv_smul_iff` that holds for `ennreal`. -/
+/-- A variant of `le_inv_smul_iff` that holds for `ENNReal`. -/
 protected theorem le_inv_smul_iff {a b : ℝ≥0∞} {r : ℝ≥0} (hr₀ : r ≠ 0) : a ≤ r⁻¹ • b ↔ r • a ≤ b :=
   by simpa [hr₀, ENNReal.smul_def] using (mul_le_iff_le_inv (coe_ne_zero.mpr hr₀) coe_ne_top).symm
 #align ennreal.le_inv_smul_iff ENNReal.le_inv_smul_iff
 
-/-- A variant of `inv_smul_le_iff` that holds for `ennreal`. -/
+/-- A variant of `inv_smul_le_iff` that holds for `ENNReal`. -/
 protected theorem inv_smul_le_iff {a b : ℝ≥0∞} {r : ℝ≥0} (hr₀ : r ≠ 0) : r⁻¹ • a ≤ b ↔ a ≤ r • b :=
   by simpa only [inv_inv] using (ENNReal.le_inv_smul_iff (inv_ne_zero hr₀)).symm
 #align ennreal.inv_smul_le_iff ENNReal.inv_smul_le_iff