From 297610838471f6ea3368bf26d2642e63a159fbcf Mon Sep 17 00:00:00 2001 From: Riccardo Brasca Date: Thu, 13 Oct 2022 11:47:31 +0000 Subject: [PATCH] chore(number_theory/number_field/basic): fix a name (#16943) This lemma is in the `ring_of_integers` namespace, so the name was redundant. --- src/number_theory/number_field/basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/number_theory/number_field/basic.lean b/src/number_theory/number_field/basic.lean index f7dca7a2d261e..5fc4093435653 100644 --- a/src/number_theory/number_field/basic.lean +++ b/src/number_theory/number_field/basic.lean @@ -102,7 +102,7 @@ integral_closure.is_integrally_closed_of_finite_extension ℚ lemma is_integral_coe (x : 𝓞 K) : is_integral ℤ (x : K) := x.2 -lemma map_mem_ring_of_integers {F L : Type*} [field L] [char_zero K] [char_zero L] +lemma map_mem {F L : Type*} [field L] [char_zero K] [char_zero L] [alg_hom_class F ℚ K L] (f : F) (x : 𝓞 K) : f x ∈ 𝓞 L := (mem_ring_of_integers _ _).2 $ map_is_integral_int f $ ring_of_integers.is_integral_coe x