Update mathlib

2024-11-29 09:55:22 +01:00
parent e20dcdbd19
commit eec4cd1ffa
3 changed files with 6 additions and 6 deletions
--- a/Nevanlinna/specialFunctions_CircleIntegral_affine.lean
+++ b/Nevanlinna/specialFunctions_CircleIntegral_affine.lean
@@ -94,9 +94,9 @@ lemma int₀

  let ρ := ‖a‖⁻¹
  have hρ : 1 < ρ := by
-    apply one_lt_inv_iff.mpr
+    apply one_lt_inv_iff₀.mpr
    constructor
-    · exact norm_pos_iff'.mpr h₁a
+    · exact norm_pos_iff.mpr h₁a
    · exact mem_ball_zero_iff.mp ha

  let F := fun z ↦ log ‖1 - z * a‖
@@ -114,7 +114,7 @@ lemma int₀
      _ < ρ * ‖a‖ := by
        apply (mul_lt_mul_right _).2
        exact mem_ball_zero_iff.mp hx
-        exact norm_pos_iff'.mpr h₁a
+        exact norm_pos_iff.mpr h₁a
      _ = 1 := by
        dsimp [ρ]
        apply inv_mul_cancel₀