Merge branch 'main' of https://github.com/AntoineChambert-Loir/Divide…

…dPowers4 into main
AntoineChambert-Loir · Jun 5, 2024 · 0dd1b86 · 0dd1b86
2 parents 7f90201 + 4aea050
commit 0dd1b86
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 27 deletions.
diff --git a/DividedPowers/ForMathlib/RingTheory/Ideal.lean b/DividedPowers/ForMathlib/RingTheory/Ideal.lean
diff --git a/unused_files/Ideal.lean b/unused_files/Ideal.lean
@@ -0,0 +1,13 @@
+import Mathlib.RingTheory.Ideal.Basic
+import Mathlib.RingTheory.Ideal.Maps
+import Mathlib.RingTheory.Ideal.Operations
+
+-- TODO : check whether we really need that
+theorem Ideal.image_eq_map_of_surjective
+    {A B : Type _} [Semiring A] [Semiring B] (f : A →+* B)
+    (I : Ideal A) (hf : Function.Surjective f) :
+    f '' I = I.map f := by
+  symm
+  ext x
+  simp only [Set.mem_image, SetLike.mem_coe]
+  apply Ideal.mem_map_iff_of_surjective _ hf