chore(ring_theory/integral_closure): fix dot notation (#14589)

leanprover-community · Jun 7, 2022 · 544fdc0 · 544fdc0
1 parent 6906627
commit 544fdc0
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 4 deletions.
diff --git a/src/number_theory/function_field.lean b/src/number_theory/function_field.lean
@@ -122,7 +122,7 @@ begin
 end
 
 lemma not_is_field : ¬ is_field (ring_of_integers Fq F) :=
-by simpa [← (is_integral.is_field_iff_is_field (is_integral_closure.is_integral_algebra Fq[X] F)
+by simpa [← ((is_integral_closure.is_integral_algebra Fq[X] F).is_field_iff_is_field
   (algebra_map_injective Fq F))] using (polynomial.not_is_field Fq)
 
 variables [function_field Fq F]

diff --git a/src/number_theory/number_field.lean b/src/number_theory/number_field.lean
@@ -111,8 +111,8 @@ begin
   have h_inj : function.injective ⇑(algebra_map ℤ (𝓞 K)),
   { exact ring_hom.injective_int (algebra_map ℤ (𝓞 K)) },
   intro hf,
-  exact int.not_is_field ((is_integral.is_field_iff_is_field
-    (is_integral_closure.is_integral_algebra ℤ K) h_inj).mpr hf)
+  exact int.not_is_field
+    (((is_integral_closure.is_integral_algebra ℤ K).is_field_iff_is_field h_inj).mpr hf)
 end
 
 instance [number_field K] : is_dedekind_domain (𝓞 K) :=

diff --git a/src/ring_theory/integral_closure.lean b/src/ring_theory/integral_closure.lean
@@ -876,7 +876,7 @@ begin
   exact ⟨y, subtype.ext_iff.mp hy⟩,
 end
 
-lemma is_integral.is_field_iff_is_field
+lemma algebra.is_integral.is_field_iff_is_field
   {R S : Type*} [comm_ring R] [nontrivial R] [comm_ring S] [is_domain S] [algebra R S]
   (H : algebra.is_integral R S) (hRS : function.injective (algebra_map R S)) :
   is_field R ↔ is_field S :=