Apply suggestions from code review

Co-authored-by: Christian Merten <[email protected]>
leanprover-community · Jan 6, 2025 · 4574791 · 4574791
1 parent 65beb30
commit 4574791
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 4 deletions.
diff --git a/Mathlib/RingTheory/Ideal/Cotangent.lean b/Mathlib/RingTheory/Ideal/Cotangent.lean
@@ -120,7 +120,7 @@ theorem cotangentIdeal_square (I : Ideal R) : I.cotangentIdeal ^ 2 = ⊥ := by
     rw [sub_zero, pow_two]; exact Ideal.mul_mem_mul hx hy
   · intro x y hx hy; exact add_mem hx hy
 
-lemma mk_mem_cotangentIdeal {I : Ideal R} {x} :
+lemma mk_mem_cotangentIdeal {I : Ideal R} {x : R} :
     Quotient.mk (I ^ 2) x ∈ I.cotangentIdeal ↔ x ∈ I := by
   refine ⟨fun ⟨y, hy, e⟩ ↦ ?_,  fun h ↦ ⟨x, h, rfl⟩⟩
   simpa using sub_mem hy (Ideal.pow_le_self two_ne_zero

diff --git a/Mathlib/RingTheory/Kaehler/CotangentComplex.lean b/Mathlib/RingTheory/Kaehler/CotangentComplex.lean
@@ -367,7 +367,7 @@ def H1Cotangent.equiv {P₁ P₂ : Extension R S} (f₁ : P₁.Hom P₂) (f₂ :
   right_inv x :=
     show (map f₁ ∘ₗ map f₂) x = LinearMap.id x by
     rw [← Extension.H1Cotangent.map_id, eq_comm, map_eq _ (f₁.comp f₂),
-    Extension.H1Cotangent.map_comp]; rfl
+      Extension.H1Cotangent.map_comp]; rfl
 
 end Extension
 

diff --git a/Mathlib/RingTheory/Smooth/Kaehler.lean b/Mathlib/RingTheory/Smooth/Kaehler.lean
@@ -519,7 +519,7 @@ lemma H1Cotangent.map_toInfinitesimal_bijective (P : Extension.{u} R S) :
 
 /--
 Given extensions `0 → I₁ → P₁ → S → 0` and `0 → I₂ → P₂ → S → 0` with `P₁` formally smooth,
-there is an arbitrary map `P₁/I₁² → P₂/I₂²` of extensions.
+this is an arbitrarily chosen map `P₁/I₁² → P₂/I₂²` of extensions.
 -/
 noncomputable
 def homInfinitesimal (P₁ P₂ : Extension R S) [FormallySmooth R P₁.Ring] :
@@ -557,7 +557,7 @@ def H1Cotangent.equivOfFormallySmooth (P₁ P₂ : Extension R S)
 
 /-- Any formally smooth extension can be used to calculate `H¹(L_{S/R})`. -/
 noncomputable
-def equivH1Cotangent (P : Extension R S) [FormallySmooth R P.Ring] :
+def equivH1CotangentOfFormallySmooth (P : Extension R S) [FormallySmooth R P.Ring] :
     P.H1Cotangent ≃ₗ[S] H1Cotangent R S :=
   have : FormallySmooth R (Generators.self R S).toExtension.Ring :=
     inferInstanceAs (FormallySmooth R (MvPolynomial _ _))