Loogle!

Result

Found 386 declarations mentioning Ideal.map. Of these, only the first 200 are shown.

• Ideal.map 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) (I : Ideal R) : Ideal S
• Ideal.map_id 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} [Semiring R] (I : Ideal R) : Ideal.map (RingHom.id R) I = I
• Ideal.map_surjective_of_surjective 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) [RingHomClass F R S] (hf : Function.Surjective ⇑f) : Function.Surjective (Ideal.map f)
• Ideal.map_idₐ 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u_3} {S : Type u_4} [CommSemiring R] [Semiring S] [Algebra R S] (I : Ideal S) : Ideal.map (AlgHom.id R S) I = I
• Ideal.IsMaximal.map_bijective 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) [RingHomClass F R S] (hf : Function.Bijective ⇑f) {I : Ideal R} : I.IsMaximal → (Ideal.map f I).IsMaximal
• Ideal.map.isMaximal 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) [RingHomClass F R S] (hf : Function.Bijective ⇑f) {I : Ideal R} : I.IsMaximal → (Ideal.map f I).IsMaximal
• Ideal.isMaximal_map_iff_of_bijective 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) [RingHomClass F R S] (hf : Function.Bijective ⇑f) {I : Ideal R} : (Ideal.map f I).IsMaximal ↔ I.IsMaximal
• Ideal.map_span 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] [RingHomClass F R S] (f : F) (s : Set R) : Ideal.map f (Ideal.span s) = Ideal.span (⇑f '' s)
• Ideal.instIsTwoSidedMapRingHomOfRingHomSurjective 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) [RingHomSurjective f] (I : Ideal R) [I.IsTwoSided] : (Ideal.map f I).IsTwoSided
• Ideal.comap_map_of_bijective 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) [RingHomClass F R S] (hf : Function.Bijective ⇑f) {I : Ideal R} : Ideal.comap f (Ideal.map f I) = I
• Ideal.map_comap_of_surjective 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) [RingHomClass F R S] (hf : Function.Surjective ⇑f) (I : Ideal S) : Ideal.map f (Ideal.comap f I) = I
• Ideal.map.eq_1 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) (I : Ideal R) : Ideal.map f I = Ideal.span (⇑f '' ↑I)
• Ideal.map_comap_map 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) (I : Ideal R) [RingHomClass F R S] : Ideal.map f (Ideal.comap f (Ideal.map f I)) = Ideal.map f I
• Ideal.comap_map_comap 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) (K : Ideal S) [RingHomClass F R S] : Ideal.comap f (Ideal.map f (Ideal.comap f K)) = Ideal.comap f K
• Ideal.map_bot 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] {f : F} [RingHomClass F R S] : Ideal.map f ⊥ = ⊥
• Ideal.map_top 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) [RingHomClass F R S] : Ideal.map f ⊤ = ⊤
• instIsPrincipalMapRingHom 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) (I : Ideal R) [Submodule.IsPrincipal I] : Submodule.IsPrincipal (Ideal.map f I)
• Ideal.map_coe 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) [RingHomClass F R S] (I : Ideal R) : Ideal.map (↑f) I = Ideal.map f I
• Ideal.map_isMaximal_of_equiv 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {E : Type u_4} [EquivLike E R S] [RingEquivClass E R S] (e : E) {p : Ideal R} [hp : p.IsMaximal] : (Ideal.map e p).IsMaximal
• Ideal.map_isPrime_of_equiv 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] {F' : Type u_4} [EquivLike F' R S] [RingEquivClass F' R S] (f : F') {I : Ideal R} [I.IsPrime] : (Ideal.map f I).IsPrime
• Ideal.le_comap_map 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] {f : F} {I : Ideal R} [RingHomClass F R S] : I ≤ Ideal.comap f (Ideal.map f I)
• Ideal.map_comap_le 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] {f : F} {K : Ideal S} [RingHomClass F R S] : Ideal.map f (Ideal.comap f K) ≤ K
• Ideal.ne_bot_of_map_ne_bot 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] {f : F} {I : Ideal R} [RingHomClass F R S] (hI : Ideal.map f I ≠ ⊥) : I ≠ ⊥
• Ideal.mem_map_of_mem 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) {I : Ideal R} {x : R} (h : x ∈ I) : f x ∈ Ideal.map f I
• Ideal.map_eq_top_or_isMaximal_of_surjective 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) [RingHomClass F R S] (hf : Function.Surjective ⇑f) {I : Ideal R} (H : I.IsMaximal) : Ideal.map f I = ⊤ ∨ (Ideal.map f I).IsMaximal
• Ideal.map_eq_bot_iff_of_injective 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u_1} {S : Type u_2} {F : Type u_3} [Semiring R] [Semiring S] [FunLike F R S] [rc : RingHomClass F R S] {I : Ideal R} {f : F} (hf : Function.Injective ⇑f) : Ideal.map f I = ⊥ ↔ I = ⊥
• Ideal.map_comap_eq_self_of_equiv 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {E : Type u_4} [EquivLike E R S] [RingEquivClass E R S] (e : E) (I : Ideal S) : Ideal.map e (Ideal.comap e I) = I
• Ideal.gc_map_comap 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) [RingHomClass F R S] : GaloisConnection (Ideal.map f) (Ideal.comap f)
• Ideal.map_iInf_comap_of_surjective 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) [RingHomClass F R S] {ι : Sort u_3} (hf : Function.Surjective ⇑f) (K : ι → Ideal S) : Ideal.map f (⨅ i, Ideal.comap f (K i)) = iInf K
• Ideal.comap_le_map_of_inverse 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) {G : Type u_2} [FunLike G S R] [RingHomClass F R S] (g : G) (I : Ideal S) (h : Function.LeftInverse ⇑g ⇑f) : Ideal.comap f I ≤ Ideal.map g I
• Ideal.map_eq_bot_iff_le_ker 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u_1} {S : Type u_2} {F : Type u_3} [Semiring R] [Semiring S] [FunLike F R S] [rc : RingHomClass F R S] {I : Ideal R} (f : F) : Ideal.map f I = ⊥ ↔ I ≤ RingHom.ker f
• Ideal.map_le_comap_of_inverse 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) {G : Type u_2} [FunLike G S R] [RingHomClass G S R] (g : G) (I : Ideal R) (h : Function.LeftInverse ⇑g ⇑f) : Ideal.map f I ≤ Ideal.comap g I
• Ideal.map_iSup 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) [RingHomClass F R S] {ι : Sort u_3} (K : ι → Ideal R) : Ideal.map f (iSup K) = ⨆ i, Ideal.map f (K i)
• Ideal.map_mono 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] {f : F} {I J : Ideal R} (h : I ≤ J) : Ideal.map f I ≤ Ideal.map f J
• Ideal.mem_image_of_mem_map_of_surjective 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) [RingHomClass F R S] (hf : Function.Surjective ⇑f) {I : Ideal R} {y : S} (H : y ∈ Ideal.map f I) : y ∈ ⇑f '' ↑I
• Ideal.giMapComap 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) [RingHomClass F R S] (hf : Function.Surjective ⇑f) : GaloisInsertion (Ideal.map f) (Ideal.comap f)
• Ideal.map_inf_comap_of_surjective 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) [RingHomClass F R S] (hf : Function.Surjective ⇑f) (I J : Ideal S) : Ideal.map f (Ideal.comap f I ⊓ Ideal.comap f J) = I ⊓ J
• Ideal.mem_map_iff_of_surjective 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) [RingHomClass F R S] (hf : Function.Surjective ⇑f) {I : Ideal R} {y : S} : y ∈ Ideal.map f I ↔ ∃ x ∈ I, f x = y
• Ideal.apply_coe_mem_map 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) (I : Ideal R) (x : ↥I) : f ↑x ∈ Ideal.map f I
• Ideal.map_radical_le 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} {F : Type u_1} [CommSemiring R] [CommSemiring S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) {I : Ideal R} : Ideal.map f I.radical ≤ (Ideal.map f I).radical
• Ideal.map_iSup_comap_of_surjective 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) [RingHomClass F R S] {ι : Sort u_3} (hf : Function.Surjective ⇑f) (K : ι → Ideal S) : Ideal.map f (⨆ i, Ideal.comap f (K i)) = iSup K
• Ideal.le_comap_of_map_le 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] {f : F} {I : Ideal R} {K : Ideal S} [RingHomClass F R S] : Ideal.map f I ≤ K → I ≤ Ideal.comap f K
• Ideal.map_le_of_le_comap 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] {f : F} {I : Ideal R} {K : Ideal S} [RingHomClass F R S] : I ≤ Ideal.comap f K → Ideal.map f I ≤ K
• Ideal.map_le_iff_le_comap 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] {f : F} {I : Ideal R} {K : Ideal S} [RingHomClass F R S] : Ideal.map f I ≤ K ↔ I ≤ Ideal.comap f K
• Ideal.map_le_comap_of_inv_on 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) {G : Type u_2} [FunLike G S R] [RingHomClass G S R] (g : G) (I : Ideal R) (hf : Set.LeftInvOn ⇑g ⇑f ↑I) : Ideal.map f I ≤ Ideal.comap g I
• Ideal.map_map 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {T : Type u_3} [Semiring T] {I : Ideal R} (f : R →+* S) (g : S →+* T) : Ideal.map g (Ideal.map f I) = Ideal.map (g.comp f) I
• Ideal.map_inf_le 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) {I J : Ideal R} [RingHomClass F R S] : Ideal.map f (I ⊓ J) ≤ Ideal.map f I ⊓ Ideal.map f J
• Ideal.le_map_of_comap_le_of_surjective 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) {I : Ideal R} {K : Ideal S} [RingHomClass F R S] (hf : Function.Surjective ⇑f) : Ideal.comap f K ≤ I → K ≤ Ideal.map f I
• Ideal.comap_le_iff_le_map 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) [RingHomClass F R S] (hf : Function.Bijective ⇑f) {I : Ideal R} {K : Ideal S} : Ideal.comap f K ≤ I ↔ K ≤ Ideal.map f I
• Ideal.map_sup 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) (I J : Ideal R) [RingHomClass F R S] : Ideal.map f (I ⊔ J) = Ideal.map f I ⊔ Ideal.map f J
• Ideal.map_isPrime_of_surjective 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u_1} {S : Type u_2} {F : Type u_3} [Ring R] [Ring S] [FunLike F R S] [rc : RingHomClass F R S] {f : F} (hf : Function.Surjective ⇑f) {I : Ideal R} [H : I.IsPrime] (hk : RingHom.ker f ≤ I) : (Ideal.map f I).IsPrime
• Ideal.comap_le_map_of_inv_on 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) {G : Type u_2} [FunLike G S R] [RingHomClass F R S] (g : G) (I : Ideal S) (hf : Set.LeftInvOn (⇑g) (⇑f) (⇑f ⁻¹' ↑I)) : Ideal.comap f I ≤ Ideal.map g I
• Ideal.comap_map_of_surjective' 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u_1} {S : Type u_2} {F : Type u_3} [Ring R] [Ring S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) (hf : Function.Surjective ⇑f) (I : Ideal R) : Ideal.comap f (Ideal.map f I) = I ⊔ RingHom.ker f
• Ideal.map_mapₐ 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u_3} {A : Type u_4} {B : Type u_5} {C : Type u_6} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] {I : Ideal A} (f : A →ₐ[R] B) (g : B →ₐ[R] C) : Ideal.map g (Ideal.map f I) = Ideal.map (g.comp f) I
• Ideal.map_sup_comap_of_surjective 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) [RingHomClass F R S] (hf : Function.Surjective ⇑f) (I J : Ideal S) : Ideal.map f (Ideal.comap f I ⊔ Ideal.comap f J) = I ⊔ J
• Ideal.mem_map_of_equiv 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {E : Type u_4} [EquivLike E R S] [RingEquivClass E R S] (e : E) {I : Ideal R} (y : S) : y ∈ Ideal.map e I ↔ ∃ x ∈ I, e x = y
• AlgHom.coe_ideal_map 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (I : Ideal A) : Ideal.map f I = Ideal.map (↑f) I
• Ideal.map_pow 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} {F : Type u_1} [CommSemiring R] [CommSemiring S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) (I : Ideal R) (n : ℕ) : Ideal.map f (I ^ n) = Ideal.map f I ^ n
• Ideal.map_sSup 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) [RingHomClass F R S] (s : Set (Ideal R)) : Ideal.map f (sSup s) = ⨆ I ∈ s, Ideal.map f I
• Ideal.comap_map_of_surjective 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} {F : Type u_1} [Ring R] [Ring S] [FunLike F R S] [RingHomClass F R S] (f : F) (hf : Function.Surjective ⇑f) (I : Ideal R) : Ideal.comap f (Ideal.map f I) = I ⊔ Ideal.comap f ⊥
• Ideal.map_eq_submodule_map 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) [h : RingHomSurjective f] (I : Ideal R) : Ideal.map f I = Submodule.map f.toSemilinearMap I
• Ideal.map_mul 📋 Mathlib.RingTheory.Ideal.Maps
  {S : Type v} {F : Type u_1} [CommSemiring S] {R : Type u_2} [Semiring R] [FunLike F R S] [RingHomClass F R S] (f : F) (I J : Ideal R) : Ideal.map f (I * J) = Ideal.map f I * Ideal.map f J
• Ideal.map_ne_bot_of_ne_bot 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u_1} [CommRing R] {S : Type u_4} [Ring S] [Nontrivial S] [Algebra R S] [NoZeroSMulDivisors R S] {I : Ideal R} (h : I ≠ ⊥) : Ideal.map (algebraMap R S) I ≠ ⊥
• Ideal.comap_map_eq_self_iff_of_isPrime 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} [CommSemiring R] {S : Type u_2} [CommSemiring S] {f : R →+* S} (p : Ideal R) [p.IsPrime] : Ideal.comap f (Ideal.map f p) = p ↔ ∃ q, q.IsPrime ∧ Ideal.comap f q = p
• Ideal.mapHom_apply 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} {F : Type u_1} [CommSemiring R] [CommSemiring S] [FunLike F R S] [rc : RingHomClass F R S] (f : F) (I : Ideal R) : (Ideal.mapHom f) I = Ideal.map f I
• Ideal.map_sInf 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u_1} {S : Type u_2} {F : Type u_3} [Ring R] [Ring S] [FunLike F R S] [rc : RingHomClass F R S] {A : Set (Ideal R)} {f : F} (hf : Function.Surjective ⇑f) : (∀ J ∈ A, RingHom.ker f ≤ J) → Ideal.map f (sInf A) = sInf (Ideal.map f '' A)
• Algebra.idealMap 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u_1} [CommSemiring R] (S : Type u_2) [Semiring S] [Algebra R S] (I : Ideal R) : ↥I →ₗ[R] ↥(Ideal.map (algebraMap R S) I)
• Ideal.map_radical_of_surjective 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {f : R →+* S} (hf : Function.Surjective ⇑f) {I : Ideal R} (h : RingHom.ker f ≤ I) : Ideal.map f I.radical = (Ideal.map f I).radical
• Ideal.apply_mem_of_equiv_iff 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {I : Ideal R} {f : R ≃+* S} {x : R} : f x ∈ Ideal.map f I ↔ x ∈ I
• Ideal.smul_top_eq_map 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u_4} {S : Type u_5} [CommSemiring R] [CommSemiring S] [Algebra R S] (I : Ideal R) : I • ⊤ = Submodule.restrictScalars R (Ideal.map (algebraMap R S) I)
• Ideal.symm_apply_mem_of_equiv_iff 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {I : Ideal R} {f : R ≃+* S} {y : S} : f.symm y ∈ I ↔ y ∈ Ideal.map f I
• Ideal.smul_restrictScalars 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u_4} {S : Type u_5} {M : Type u_6} [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower R S M] (I : Ideal R) (N : Submodule S M) : Submodule.restrictScalars R (Ideal.map (algebraMap R S) I • N) = I • Submodule.restrictScalars R N
• Ideal.map_eq_iff_sup_ker_eq_of_surjective 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {I J : Ideal R} (f : R →+* S) (hf : Function.Surjective ⇑f) : Ideal.map f I = Ideal.map f J ↔ I ⊔ RingHom.ker f = J ⊔ RingHom.ker f
• Ideal.comap_symm 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {I : Ideal R} (f : R ≃+* S) : Ideal.comap f.symm I = Ideal.map f I
• Ideal.map_symm 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {I : Ideal S} (f : R ≃+* S) : Ideal.map f.symm I = Ideal.comap f I
• Ideal.map_comap_of_equiv 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {I : Ideal R} (f : R ≃+* S) : Ideal.map (↑f) I = Ideal.comap f.symm I
• Ideal.map_of_equiv 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {I : Ideal R} (f : R ≃+* S) : Ideal.map (↑f.symm) (Ideal.map (↑f) I) = I
• Algebra.idealMap_apply_coe 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u_1} [CommSemiring R] (S : Type u_2) [Semiring S] [Algebra R S] (I : Ideal R) (c : ↥I) : ↑((Algebra.idealMap S I) c) = (algebraMap R S) ↑c
• Ideal.map_fst_prod 📋 Mathlib.RingTheory.Ideal.Prod
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (I : Ideal R) (J : Ideal S) : Ideal.map (RingHom.fst R S) (I.prod J) = I
• Ideal.map_snd_prod 📋 Mathlib.RingTheory.Ideal.Prod
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (I : Ideal R) (J : Ideal S) : Ideal.map (RingHom.snd R S) (I.prod J) = J
• Ideal.ideal_prod_eq 📋 Mathlib.RingTheory.Ideal.Prod
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (I : Ideal (R × S)) : I = (Ideal.map (RingHom.fst R S) I).prod (Ideal.map (RingHom.snd R S) I)
• Ideal.map_prodComm_prod 📋 Mathlib.RingTheory.Ideal.Prod
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (I : Ideal R) (J : Ideal S) : Ideal.map (↑RingEquiv.prodComm) (I.prod J) = J.prod I
• Submodule.IsPrincipal.map_ringHom 📋 Mathlib.RingTheory.PrincipalIdealDomain
  {R : Type u} {S : Type u_1} {F : Type u_3} [Ring R] [Ring S] [FunLike F R S] [RingHomClass F R S] (f : F) {I : Ideal R} (hI : Submodule.IsPrincipal I) : Submodule.IsPrincipal (Ideal.map f I)
• Ideal.isPrime_map_C_of_isPrime 📋 Mathlib.RingTheory.Polynomial.Basic
  {R : Type u} [CommRing R] {P : Ideal R} (H : P.IsPrime) : (Ideal.map Polynomial.C P).IsPrime
• Ideal.isPrime_map_C_iff_isPrime 📋 Mathlib.RingTheory.Polynomial.Basic
  {R : Type u} [CommRing R] (P : Ideal R) : (Ideal.map Polynomial.C P).IsPrime ↔ P.IsPrime
• Ideal.mem_map_C_iff 📋 Mathlib.RingTheory.Polynomial.Basic
  {R : Type u} [CommSemiring R] {I : Ideal R} {f : Polynomial R} : f ∈ Ideal.map Polynomial.C I ↔ ∀ (n : ℕ), f.coeff n ∈ I
• Polynomial.ker_mapRingHom 📋 Mathlib.RingTheory.Polynomial.Basic
  {R : Type u} {S : Type u_1} [CommSemiring R] [Semiring S] (f : R →+* S) : RingHom.ker (Polynomial.mapRingHom f) = Ideal.map Polynomial.C (RingHom.ker f)
• MvPolynomial.mem_map_C_iff 📋 Mathlib.RingTheory.Polynomial.Basic
  {R : Type u} {σ : Type v} [CommRing R] {I : Ideal R} {f : MvPolynomial σ R} : f ∈ Ideal.map MvPolynomial.C I ↔ ∀ (m : σ →₀ ℕ), MvPolynomial.coeff m f ∈ I
• MvPolynomial.ker_map 📋 Mathlib.RingTheory.Polynomial.Basic
  {R : Type u} {S : Type u_1} {σ : Type v} [CommRing R] [CommRing S] (f : R →+* S) : RingHom.ker (MvPolynomial.map f) = Ideal.map MvPolynomial.C (RingHom.ker f)
• MvPolynomial.ker_mapAlgHom 📋 Mathlib.RingTheory.Polynomial.Basic
  {R : Type u} [CommRing R] {S₁ : Type u_2} {S₂ : Type u_3} {σ : Type u_4} [CommRing S₁] [CommRing S₂] [Algebra R S₁] [Algebra R S₂] (f : S₁ →ₐ[R] S₂) : RingHom.ker (MvPolynomial.mapAlgHom f) = Ideal.map MvPolynomial.C (RingHom.ker f)
• Ideal.quotientEquivAlg 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R₁] [Ring A] [Algebra R₁ A] [Ring B] [Algebra R₁ B] (I : Ideal A) (J : Ideal B) [I.IsTwoSided] [J.IsTwoSided] (f : A ≃ₐ[R₁] B) (hIJ : J = Ideal.map (↑f) I) : (A ⧸ I) ≃ₐ[R₁] B ⧸ J
• Ideal.map_quotient_self 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  {R : Type u} [Ring R] (I : Ideal R) [I.IsTwoSided] : Ideal.map (Ideal.Quotient.mk I) I = ⊥
• Ideal.map_mk_eq_bot_of_le 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  {R : Type u} [Ring R] {I J : Ideal R} [J.IsTwoSided] (h : I ≤ J) : Ideal.map (Ideal.Quotient.mk J) I = ⊥
• Ideal.comap_map_mk 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  {R : Type u} [Ring R] {I J : Ideal R} [I.IsTwoSided] (h : I ≤ J) : Ideal.comap (Ideal.Quotient.mk I) (Ideal.map (Ideal.Quotient.mk I) J) = J
• Ideal.ker_quotient_lift 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  {R : Type u} {S : Type v} [Ring R] [Semiring S] {I : Ideal R} [I.IsTwoSided] (f : R →+* S) (H : I ≤ RingHom.ker f) : RingHom.ker (Ideal.Quotient.lift I f H) = Ideal.map (Ideal.Quotient.mk I) (RingHom.ker f)
• Ideal.mem_quotient_iff_mem_sup 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  {R : Type u} [Ring R] {I J : Ideal R} [I.IsTwoSided] {x : R} : (Ideal.Quotient.mk I) x ∈ Ideal.map (Ideal.Quotient.mk I) J ↔ x ∈ J ⊔ I
• Ideal.mem_quotient_iff_mem 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  {R : Type u} [Ring R] {I J : Ideal R} [I.IsTwoSided] (hIJ : I ≤ J) {x : R} : (Ideal.Quotient.mk I) x ∈ Ideal.map (Ideal.Quotient.mk I) J ↔ x ∈ J
• DoubleQuot.quotQuotMkₐ 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I J : Ideal A) : A →ₐ[R] (A ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mkₐ R I) J
• DoubleQuot.quotQuotMk 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  {R : Type u} [CommRing R] (I J : Ideal R) : R →+* (R ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J
• Ideal.quotientEquiv 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  {R : Type u} [Ring R] {S : Type v} [Ring S] (I : Ideal R) (J : Ideal S) [I.IsTwoSided] [J.IsTwoSided] (f : R ≃+* S) (hIJ : J = Ideal.map (↑f) I) : R ⧸ I ≃+* S ⧸ J
• DoubleQuot.quotQuotEquivQuotOfLEₐ 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] {I J : Ideal A} (h : I ≤ J) : ((A ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mkₐ R I) J) ≃ₐ[R] A ⧸ J
• DoubleQuot.liftSupQuotQuotMkₐ 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I J : Ideal A) : A ⧸ I ⊔ J →ₐ[R] (A ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mkₐ R I) J
• DoubleQuot.quotQuotEquivQuotSupₐ 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I J : Ideal A) : ((A ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mkₐ R I) J) ≃ₐ[R] A ⧸ I ⊔ J
• DoubleQuot.quotQuotToQuotSupₐ 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I J : Ideal A) : (A ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mkₐ R I) J →ₐ[R] A ⧸ I ⊔ J
• DoubleQuot.liftSupQuotQuotMk 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  {R : Type u} [CommRing R] (I J : Ideal R) : R ⧸ I ⊔ J →+* (R ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J
• DoubleQuot.quotQuotToQuotSup 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  {R : Type u} [CommRing R] (I J : Ideal R) : (R ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J →+* R ⧸ I ⊔ J
• DoubleQuot.ker_quotLeftToQuotSup 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  {R : Type u} [CommRing R] (I J : Ideal R) : RingHom.ker (DoubleQuot.quotLeftToQuotSup I J) = Ideal.map (Ideal.Quotient.mk I) J
• DoubleQuot.quotQuotEquivCommₐ 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I J : Ideal A) : ((A ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mkₐ R I) J) ≃ₐ[R] (A ⧸ J) ⧸ Ideal.map (Ideal.Quotient.mkₐ R J) I
• Ideal.quotientEquiv_mk 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  {R : Type u} [Ring R] {S : Type v} [Ring S] (I : Ideal R) (J : Ideal S) [I.IsTwoSided] [J.IsTwoSided] (f : R ≃+* S) (hIJ : J = Ideal.map (↑f) I) (x : R) : (I.quotientEquiv J f hIJ) ((Ideal.Quotient.mk I) x) = (Ideal.Quotient.mk J) (f x)
• Ideal.quotientEquiv_apply 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  {R : Type u} [Ring R] {S : Type v} [Ring S] (I : Ideal R) (J : Ideal S) [I.IsTwoSided] [J.IsTwoSided] (f : R ≃+* S) (hIJ : J = Ideal.map (↑f) I) (a✝ : R ⧸ I) : (I.quotientEquiv J f hIJ) a✝ = (↑↑(Ideal.quotientMap J ↑f ⋯)).toFun a✝
• DoubleQuot.quotQuotMk.eq_1 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  {R : Type u} [CommRing R] (I J : Ideal R) : DoubleQuot.quotQuotMk I J = (Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk I) J)).comp (Ideal.Quotient.mk I)
• Ideal.quotientEquiv_symm_mk 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  {R : Type u} [Ring R] {S : Type v} [Ring S] (I : Ideal R) (J : Ideal S) [I.IsTwoSided] [J.IsTwoSided] (f : R ≃+* S) (hIJ : J = Ideal.map (↑f) I) (x : S) : (I.quotientEquiv J f hIJ).symm ((Ideal.Quotient.mk J) x) = (Ideal.Quotient.mk I) (f.symm x)
• Ideal.quotientEquiv_symm_apply 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  {R : Type u} [Ring R] {S : Type v} [Ring S] (I : Ideal R) (J : Ideal S) [I.IsTwoSided] [J.IsTwoSided] (f : R ≃+* S) (hIJ : J = Ideal.map (↑f) I) (a : S ⧸ J) : (I.quotientEquiv J f hIJ).symm a = (Ideal.quotientMap I ↑f.symm ⋯) a
• DoubleQuot.ker_quotQuotMk 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  {R : Type u} [CommRing R] (I J : Ideal R) : RingHom.ker (DoubleQuot.quotQuotMk I J) = I ⊔ J
• DoubleQuot.quotQuotEquivComm_symmₐ 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I J : Ideal A) : (DoubleQuot.quotQuotEquivCommₐ R I J).symm = DoubleQuot.quotQuotEquivCommₐ R J I
• DoubleQuot.coe_quotQuotMkₐ 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I J : Ideal A) : ⇑(DoubleQuot.quotQuotMkₐ R I J) = ⇑(DoubleQuot.quotQuotMk I J)
• DoubleQuot.quotQuotEquivQuotOfLE 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  {R : Type u} [CommRing R] {I J : Ideal R} (h : I ≤ J) : (R ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J ≃+* R ⧸ J
• Ideal.ker_quotientMap_mk 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  {R : Type u} [Ring R] {I J : Ideal R} [I.IsTwoSided] [J.IsTwoSided] : RingHom.ker (Ideal.quotientMap (Ideal.map (Ideal.Quotient.mk I) J) (Ideal.Quotient.mk I) ⋯) = Ideal.map (Ideal.Quotient.mk J) I
• DoubleQuot.coe_liftSupQuotQuotMkₐ 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I J : Ideal A) : ⇑(DoubleQuot.liftSupQuotQuotMkₐ R I J) = ⇑(DoubleQuot.liftSupQuotQuotMk I J)
• DoubleQuot.quotQuotEquivQuotSup 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  {R : Type u} [CommRing R] (I J : Ideal R) : (R ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J ≃+* R ⧸ I ⊔ J
• DoubleQuot.coe_quotQuotToQuotSupₐ 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I J : Ideal A) : ⇑(DoubleQuot.quotQuotToQuotSupₐ R I J) = ⇑(DoubleQuot.quotQuotToQuotSup I J)
• DoubleQuot.quotQuotMkₐ_toRingHom 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I J : Ideal A) : ↑(DoubleQuot.quotQuotMkₐ R I J) = DoubleQuot.quotQuotMk I J
• DoubleQuot.quotQuotEquivQuotOfLE_comp_quotQuotMkₐ 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] {I J : Ideal A} (h : I ≤ J) : (↑(DoubleQuot.quotQuotEquivQuotOfLEₐ R h)).comp (DoubleQuot.quotQuotMkₐ R I J) = Ideal.Quotient.mkₐ R J
• Ideal.powQuotPowSuccEquivMapMkPowSuccPow 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  {R : Type u_1} [CommRing R] (I : Ideal R) (n : ℕ) : ↥(I ^ n) ⧸ I • ⊤ ≃ ↥(Ideal.map (Ideal.Quotient.mk (I ^ (n + 1))) (I ^ n))
• DoubleQuot.liftSupQuotQuotMkₐ_toRingHom 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I J : Ideal A) : ↑(DoubleQuot.liftSupQuotQuotMkₐ R I J) = DoubleQuot.liftSupQuotQuotMk I J
• DoubleQuot.quotQuotToQuotSupₐ_toRingHom 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I J : Ideal A) : ↑(DoubleQuot.quotQuotToQuotSupₐ R I J) = DoubleQuot.quotQuotToQuotSup I J
• DoubleQuot.quotQuotEquivQuotOfLE_symm_comp_mkₐ 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] {I J : Ideal A} (h : I ≤ J) : (↑(DoubleQuot.quotQuotEquivQuotOfLEₐ R h).symm).comp (Ideal.Quotient.mkₐ R J) = DoubleQuot.quotQuotMkₐ R I J
• DoubleQuot.quotQuotEquivComm 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  {R : Type u} [CommRing R] (I J : Ideal R) : (R ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J ≃+* (R ⧸ J) ⧸ Ideal.map (Ideal.Quotient.mk J) I
• DoubleQuot.quotQuotEquivComm_comp_quotQuotMkₐ 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I J : Ideal A) : (↑(DoubleQuot.quotQuotEquivCommₐ R I J)).comp (DoubleQuot.quotQuotMkₐ R I J) = DoubleQuot.quotQuotMkₐ R J I
• DoubleQuot.quotQuotEquivQuotOfLEₐ_toRingEquiv 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] {I J : Ideal A} (h : I ≤ J) : ↑(DoubleQuot.quotQuotEquivQuotOfLEₐ R h) = DoubleQuot.quotQuotEquivQuotOfLE h
• DoubleQuot.quotQuotEquivQuotSupₐ_toRingEquiv 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I J : Ideal A) : ↑(DoubleQuot.quotQuotEquivQuotSupₐ R I J) = DoubleQuot.quotQuotEquivQuotSup I J
• DoubleQuot.quotQuotEquivQuotOfLE_quotQuotMk 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  {R : Type u} [CommRing R] {I J : Ideal R} (x : R) (h : I ≤ J) : (DoubleQuot.quotQuotEquivQuotOfLE h) ((DoubleQuot.quotQuotMk I J) x) = (Ideal.Quotient.mk J) x
• DoubleQuot.quotQuotEquivComm_symm 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  {R : Type u} [CommRing R] (I J : Ideal R) : (DoubleQuot.quotQuotEquivComm I J).symm = DoubleQuot.quotQuotEquivComm J I
• DoubleQuot.coe_quotQuotEquivQuotOfLEₐ 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] {I J : Ideal A} (h : I ≤ J) : ⇑(DoubleQuot.quotQuotEquivQuotOfLEₐ R h) = ⇑(DoubleQuot.quotQuotEquivQuotOfLE h)
• DoubleQuot.quotQuotEquivQuotOfLEₐ_symm_toRingEquiv 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] {I J : Ideal A} (h : I ≤ J) : ↑(DoubleQuot.quotQuotEquivQuotOfLEₐ R h).symm = (DoubleQuot.quotQuotEquivQuotOfLE h).symm
• DoubleQuot.quotQuotEquivQuotSup_quotQuotMk 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  {R : Type u} [CommRing R] (I J : Ideal R) (x : R) : (DoubleQuot.quotQuotEquivQuotSup I J) ((DoubleQuot.quotQuotMk I J) x) = (Ideal.Quotient.mk (I ⊔ J)) x
• DoubleQuot.coe_quotQuotEquivQuotSupₐ 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I J : Ideal A) : ⇑(DoubleQuot.quotQuotEquivQuotSupₐ R I J) = ⇑(DoubleQuot.quotQuotEquivQuotSup I J)
• DoubleQuot.quotQuotEquivQuotSup_quot_quot_algebraMap 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  {R : Type u} [CommSemiring R] {A : Type v} [CommRing A] [Algebra R A] (I J : Ideal A) (x : R) : (DoubleQuot.quotQuotEquivQuotSup I J) ((algebraMap R ((A ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J)) x) = (algebraMap R (A ⧸ I ⊔ J)) x
• DoubleQuot.quotQuotEquivQuotOfLE_symm_mk 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  {R : Type u} [CommRing R] {I J : Ideal R} (x : R) (h : I ≤ J) : (DoubleQuot.quotQuotEquivQuotOfLE h).symm ((Ideal.Quotient.mk J) x) = (DoubleQuot.quotQuotMk I J) x
• DoubleQuot.coe_quotQuotEquivQuotOfLEₐ_symm 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] {I J : Ideal A} (h : I ≤ J) : ⇑(DoubleQuot.quotQuotEquivQuotOfLEₐ R h).symm = ⇑(DoubleQuot.quotQuotEquivQuotOfLE h).symm
• DoubleQuot.quotQuotEquivQuotSupₐ_symm_toRingEquiv 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I J : Ideal A) : ↑(DoubleQuot.quotQuotEquivQuotSupₐ R I J).symm = (DoubleQuot.quotQuotEquivQuotSup I J).symm
• Ideal.powQuotPowSuccLinearEquivMapMkPowSuccPow 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  {R : Type u_1} [CommRing R] (I : Ideal R) (n : ℕ) : (↥(I ^ n) ⧸ I • ⊤) ≃ₗ[R] ↥(Ideal.map (Ideal.Quotient.mk (I ^ (n + 1))) (I ^ n))
• DoubleQuot.quotQuotEquivQuotSup_symm_quotQuotMk 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  {R : Type u} [CommRing R] (I J : Ideal R) (x : R) : (DoubleQuot.quotQuotEquivQuotSup I J).symm ((Ideal.Quotient.mk (I ⊔ J)) x) = (DoubleQuot.quotQuotMk I J) x
• DoubleQuot.coe_quotQuotEquivQuotSupₐ_symm 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I J : Ideal A) : ⇑(DoubleQuot.quotQuotEquivQuotSupₐ R I J).symm = ⇑(DoubleQuot.quotQuotEquivQuotSup I J).symm
• DoubleQuot.quotQuotEquivCommₐ_toRingEquiv 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I J : Ideal A) : ↑(DoubleQuot.quotQuotEquivCommₐ R I J) = DoubleQuot.quotQuotEquivComm I J
• DoubleQuot.quotQuotEquivQuotOfLE_comp_quotQuotMk 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  {R : Type u} [CommRing R] {I J : Ideal R} (h : I ≤ J) : (↑(DoubleQuot.quotQuotEquivQuotOfLE h)).comp (DoubleQuot.quotQuotMk I J) = Ideal.Quotient.mk J
• DoubleQuot.quotQuotEquivComm_quotQuotMk 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  {R : Type u} [CommRing R] (I J : Ideal R) (x : R) : (DoubleQuot.quotQuotEquivComm I J) ((DoubleQuot.quotQuotMk I J) x) = (DoubleQuot.quotQuotMk J I) x
• DoubleQuot.coe_quotQuotEquivCommₐ 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  (R : Type u) {A : Type u_1} [CommSemiring R] [CommRing A] [Algebra R A] (I J : Ideal A) : ⇑(DoubleQuot.quotQuotEquivCommₐ R I J) = ⇑(DoubleQuot.quotQuotEquivComm I J)
• DoubleQuot.quotQuotEquivComm_algebraMap 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  {R : Type u} [CommSemiring R] {A : Type v} [CommRing A] [Algebra R A] (I J : Ideal A) (x : R) : (DoubleQuot.quotQuotEquivComm I J) ((algebraMap R ((A ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J)) x) = (algebraMap R ((A ⧸ J) ⧸ Ideal.map (Ideal.Quotient.mk J) I)) x
• DoubleQuot.quotQuotEquivComm_mk_mk 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  {R : Type u} [CommRing R] (I J : Ideal R) (x : R) : (DoubleQuot.quotQuotEquivComm I J) ((Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk I) J)) ((Ideal.Quotient.mk I) x)) = (algebraMap R ((R ⧸ J) ⧸ Ideal.map (Ideal.Quotient.mk J) I)) x
• DoubleQuot.quotQuotEquivQuotOfLE_symm_comp_mk 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  {R : Type u} [CommRing R] {I J : Ideal R} (h : I ≤ J) : (↑(DoubleQuot.quotQuotEquivQuotOfLE h).symm).comp (Ideal.Quotient.mk J) = DoubleQuot.quotQuotMk I J
• DoubleQuot.quotQuotEquivComm_comp_quotQuotMk 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  {R : Type u} [CommRing R] (I J : Ideal R) : (↑(DoubleQuot.quotQuotEquivComm I J)).comp (DoubleQuot.quotQuotMk I J) = DoubleQuot.quotQuotMk J I
• Ideal.map_jacobson_of_bijective 📋 Mathlib.RingTheory.Jacobson.Ideal
  {R : Type u} {S : Type v} [Ring R] [Ring S] {I : Ideal R} {f : R →+* S} (hf : Function.Bijective ⇑f) : Ideal.map f I.jacobson = (Ideal.map f I).jacobson
• Ideal.map_jacobson_of_surjective 📋 Mathlib.RingTheory.Jacobson.Ideal
  {R : Type u} {S : Type v} [Ring R] [Ring S] {I : Ideal R} {f : R →+* S} (hf : Function.Surjective ⇑f) : RingHom.ker f ≤ I → Ideal.map f I.jacobson = (Ideal.map f I).jacobson
• IsLocalRing.local_hom_TFAE 📋 Mathlib.RingTheory.LocalRing.RingHom.Basic
  {R : Type u_1} {S : Type u_2} [CommSemiring R] [IsLocalRing R] [CommSemiring S] [IsLocalRing S] (f : R →+* S) : [IsLocalHom f, ⇑f '' ↑(IsLocalRing.maximalIdeal R).toAddSubmonoid ⊆ ↑(IsLocalRing.maximalIdeal S), Ideal.map f (IsLocalRing.maximalIdeal R) ≤ IsLocalRing.maximalIdeal S, IsLocalRing.maximalIdeal R ≤ Ideal.comap f (IsLocalRing.maximalIdeal S), Ideal.comap f (IsLocalRing.maximalIdeal S) = IsLocalRing.maximalIdeal R].TFAE
• LocalRing.local_hom_TFAE 📋 Mathlib.RingTheory.LocalRing.RingHom.Basic
  {R : Type u_1} {S : Type u_2} [CommSemiring R] [IsLocalRing R] [CommSemiring S] [IsLocalRing S] (f : R →+* S) : [IsLocalHom f, ⇑f '' ↑(IsLocalRing.maximalIdeal R).toAddSubmonoid ⊆ ↑(IsLocalRing.maximalIdeal S), Ideal.map f (IsLocalRing.maximalIdeal R) ≤ IsLocalRing.maximalIdeal S, IsLocalRing.maximalIdeal R ≤ Ideal.comap f (IsLocalRing.maximalIdeal S), Ideal.comap f (IsLocalRing.maximalIdeal S) = IsLocalRing.maximalIdeal R].TFAE
• Algebra.TensorProduct.lTensor_ker 📋 Mathlib.LinearAlgebra.TensorProduct.RightExactness
  {R : Type u_4} [CommRing R] {A : Type u_5} {C : Type u_7} {D : Type u_8} [Ring A] [Ring C] [Ring D] [Algebra R A] [Algebra R C] [Algebra R D] (g : C →ₐ[R] D) (hg : Function.Surjective ⇑g) : RingHom.ker (Algebra.TensorProduct.map (AlgHom.id R A) g) = Ideal.map Algebra.TensorProduct.includeRight (RingHom.ker g)
• Algebra.TensorProduct.rTensor_ker 📋 Mathlib.LinearAlgebra.TensorProduct.RightExactness
  {R : Type u_4} [CommRing R] {A : Type u_5} {B : Type u_6} {C : Type u_7} [Ring A] [Ring B] [Ring C] [Algebra R A] [Algebra R B] [Algebra R C] (f : A →ₐ[R] B) (hf : Function.Surjective ⇑f) : RingHom.ker (Algebra.TensorProduct.map f (AlgHom.id R C)) = Ideal.map Algebra.TensorProduct.includeLeft (RingHom.ker f)
• Algebra.TensorProduct.map_ker 📋 Mathlib.LinearAlgebra.TensorProduct.RightExactness
  {R : Type u_4} [CommRing R] {A : Type u_5} {B : Type u_6} {C : Type u_7} {D : Type u_8} [Ring A] [Ring B] [Ring C] [Ring D] [Algebra R A] [Algebra R B] [Algebra R C] [Algebra R D] (f : A →ₐ[R] B) (g : C →ₐ[R] D) (hf : Function.Surjective ⇑f) (hg : Function.Surjective ⇑g) : RingHom.ker (Algebra.TensorProduct.map f g) = Ideal.map Algebra.TensorProduct.includeLeft (RingHom.ker f) ⊔ Ideal.map Algebra.TensorProduct.includeRight (RingHom.ker g)
• Ideal.map_includeRight_eq 📋 Mathlib.LinearAlgebra.TensorProduct.RightExactness
  {R : Type u_1} [CommSemiring R] {A : Type u_2} {B : Type u_3} [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (I : Ideal B) : Submodule.restrictScalars R (Ideal.map Algebra.TensorProduct.includeRight I) = LinearMap.range (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype)
• Ideal.map_includeLeft_eq 📋 Mathlib.LinearAlgebra.TensorProduct.RightExactness
  {R : Type u_1} [CommSemiring R] {A : Type u_2} {B : Type u_3} [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (I : Ideal A) : Submodule.restrictScalars R (Ideal.map Algebra.TensorProduct.includeLeft I) = LinearMap.range (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype)
• Ideal.FG.map 📋 Mathlib.RingTheory.Finiteness.Ideal
  {R : Type u_3} {S : Type u_4} [Semiring R] [Semiring S] {I : Ideal R} (h : I.FG) (f : R →+* S) : (Ideal.map f I).FG
• IsLocalization.map_radical 📋 Mathlib.RingTheory.Localization.Ideal
  {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] (I : Ideal R) : Ideal.map (algebraMap R S) I.radical = (Ideal.map (algebraMap R S) I).radical
• IsLocalization.map_comap 📋 Mathlib.RingTheory.Localization.Ideal
  {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] (J : Ideal S) : Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) J) = J
• IsLocalization.isPrime_of_isPrime_disjoint 📋 Mathlib.RingTheory.Localization.Ideal
  {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] (I : Ideal R) (hp : I.IsPrime) (hd : Disjoint ↑M ↑I) : (Ideal.map (algebraMap R S) I).IsPrime
• IsLocalization.map_algebraMap_ne_top_iff_disjoint 📋 Mathlib.RingTheory.Localization.Ideal
  {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] (I : Ideal R) : Ideal.map (algebraMap R S) I ≠ ⊤ ↔ Disjoint ↑M ↑I
• IsLocalization.comap_map_of_isPrime_disjoint 📋 Mathlib.RingTheory.Localization.Ideal
  {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] (I : Ideal R) (hI : I.IsPrime) (hM : Disjoint ↑M ↑I) : Ideal.comap (algebraMap R S) (Ideal.map (algebraMap R S) I) = I
• IsLocalization.algebraMap_mem_map_algebraMap_iff 📋 Mathlib.RingTheory.Localization.Ideal
  {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] (I : Ideal R) (x : R) : (algebraMap R S) x ∈ Ideal.map (algebraMap R S) I ↔ ∃ m ∈ M, m * x ∈ I
• IsLocalization.mk'_mem_map_algebraMap_iff 📋 Mathlib.RingTheory.Localization.Ideal
  {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] (I : Ideal R) (x : R) (s : ↥M) : IsLocalization.mk' S x s ∈ Ideal.map (algebraMap R S) I ↔ ∃ s ∈ M, s * x ∈ I
• IsLocalization.ideal_eq_iInf_comap_map_away 📋 Mathlib.RingTheory.Localization.Ideal
  {R : Type u_1} [CommSemiring R] {S : Finset R} (hS : Ideal.span ↑S = ⊤) (I : Ideal R) : I = ⨅ f ∈ S, Ideal.comap (algebraMap R (Localization.Away f)) (Ideal.map (algebraMap R (Localization.Away f)) I)
• IsLocalization.mem_map_algebraMap_iff 📋 Mathlib.RingTheory.Localization.Ideal
  {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] {I : Ideal R} {z : S} : z ∈ Ideal.map (algebraMap R S) I ↔ ∃ x, z * (algebraMap R S) ↑x.2 = (algebraMap R S) ↑x.1
• IsLocalization.of_surjective 📋 Mathlib.RingTheory.Localization.Ideal
  {R : Type u_1} [CommRing R] (M : Submonoid R) (S : Type u_2) [CommRing S] [Algebra R S] [IsLocalization M S] {R' : Type u_3} {S' : Type u_4} [CommRing R'] [CommRing S'] [Algebra R' S'] (f : R →+* R') (hf : Function.Surjective ⇑f) (g : S →+* S') (hg : Function.Surjective ⇑g) (H : g.comp (algebraMap R S) = (algebraMap R' S').comp f) (H' : RingHom.ker g ≤ Ideal.map (algebraMap R S) (RingHom.ker f)) : IsLocalization (Submonoid.map f M) S'
• Ideal.pointwise_smul_def 📋 Mathlib.RingTheory.Ideal.Pointwise
  {M : Type u_1} {R : Type u_2} [Monoid M] [Semiring R] [MulSemiringAction M R] {a : M} (S : Ideal R) : a • S = Ideal.map (MulSemiringAction.toRingHom M R a) S
• Ideal.map_equiv_liesOver 📋 Mathlib.RingTheory.Ideal.Over
  {A : Type u_2} [CommSemiring A] {B : Type u_3} {C : Type u_4} [Semiring B] [Semiring C] [Algebra A B] [Algebra A C] (P : Ideal B) (p : Ideal A) [P.LiesOver p] {E : Type u_5} [EquivLike E B C] [AlgEquivClass E A B C] (σ : E) : (Ideal.map σ P).LiesOver p
• Ideal.LiesOver.of_eq_map_equiv 📋 Mathlib.RingTheory.Ideal.Over
  {A : Type u_2} [CommSemiring A] {B : Type u_3} {C : Type u_4} [Semiring B] [Semiring C] [Algebra A B] [Algebra A C] {P : Ideal B} {Q : Ideal C} (p : Ideal A) [P.LiesOver p] {E : Type u_5} [EquivLike E B C] [AlgEquivClass E A B C] (σ : E) (h : Q = Ideal.map σ P) : Q.LiesOver p
• Ideal.Quotient.algebraQuotientMapQuotient 📋 Mathlib.RingTheory.Ideal.Over
  {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {p : Ideal R} [Algebra R S] : Algebra (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
• Ideal.Quotient.algEquivOfEqMap 📋 Mathlib.RingTheory.Ideal.Over
  {A : Type u_3} {B : Type u_4} {C : Type u_5} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra A C] {P : Ideal B} {Q : Ideal C} (p : Ideal A) [Q.LiesOver p] [P.LiesOver p] {E : Type u_7} [EquivLike E B C] [AlgEquivClass E A B C] (σ : E) (h : Q = Ideal.map σ P) : (B ⧸ P) ≃ₐ[A ⧸ p] C ⧸ Q
• Ideal.Quotient.tower_quotient_map_quotient 📋 Mathlib.RingTheory.Ideal.Over
  {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {p : Ideal R} [Algebra R S] : IsScalarTower R (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
• Ideal.Quotient.algEquivOfEqMap_apply 📋 Mathlib.RingTheory.Ideal.Over
  {A : Type u_3} {B : Type u_4} {C : Type u_5} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra A C] {P : Ideal B} {Q : Ideal C} (p : Ideal A) [Q.LiesOver p] [P.LiesOver p] {E : Type u_7} [EquivLike E B C] [AlgEquivClass E A B C] (σ : E) (h : Q = Ideal.map σ P) (x : B) : (Ideal.Quotient.algEquivOfEqMap p σ h) ((Ideal.Quotient.mk P) x) = (Ideal.Quotient.mk Q) (σ x)
• Ideal.Quotient.algebraMap_quotient_map_quotient 📋 Mathlib.RingTheory.Ideal.Over
  {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {p : Ideal R} [Algebra R S] (x : R) : (algebraMap (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)) ((Ideal.Quotient.mk p) x) = (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) ((algebraMap R S) x)
• Ideal.Quotient.mk_smul_mk_quotient_map_quotient 📋 Mathlib.RingTheory.Ideal.Over
  {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {p : Ideal R} [Algebra R S] (x : R) (y : S) : (Ideal.Quotient.mk p) x • (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) y = (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) ((algebraMap R S) x * y)
• Ideal.isPrime_map_of_isLocalizationAtPrime 📋 Mathlib.RingTheory.Localization.AtPrime
  {R : Type u_4} [CommRing R] (q : Ideal R) [q.IsPrime] {S : Type u_5} [CommRing S] [Algebra R S] [IsLocalization.AtPrime S q] {p : Ideal R} [p.IsPrime] (hpq : p ≤ q) : (Ideal.map (algebraMap R S) p).IsPrime
• Ideal.under_map_of_isLocalizationAtPrime 📋 Mathlib.RingTheory.Localization.AtPrime
  {R : Type u_4} [CommRing R] (q : Ideal R) [q.IsPrime] {S : Type u_5} [CommRing S] [Algebra R S] [IsLocalization.AtPrime S q] {p : Ideal R} [p.IsPrime] (hpq : p ≤ q) : Ideal.under R (Ideal.map (algebraMap R S) p) = p
• Localization.AtPrime.map_eq_maximalIdeal 📋 Mathlib.RingTheory.Localization.AtPrime
  {R : Type u_1} [CommSemiring R] {I : Ideal R} [hI : I.IsPrime] : Ideal.map (algebraMap R (Localization.AtPrime I)) I = IsLocalRing.maximalIdeal (Localization I.primeCompl)
• Ideal.localized'_eq_map 📋 Mathlib.RingTheory.LocalProperties.Basic
  {R : Type u_1} (S : Type u_2) [CommSemiring R] [CommSemiring S] [Algebra R S] (p : Submonoid R) [IsLocalization p S] (I : Ideal R) : Submodule.localized' S p (Algebra.linearMap R S) I = Ideal.map (algebraMap R S) I
• Ideal.localized₀_eq_restrictScalars_map 📋 Mathlib.RingTheory.LocalProperties.Basic
  {R : Type u_1} (S : Type u_2) [CommSemiring R] [CommSemiring S] [Algebra R S] (p : Submonoid R) [IsLocalization p S] (I : Ideal R) : Submodule.localized₀ p (Algebra.linearMap R S) I = Submodule.restrictScalars R (Ideal.map (algebraMap R S) I)
• ideal_eq_bot_of_localization' 📋 Mathlib.RingTheory.LocalProperties.Basic
  {R : Type u_1} [CommSemiring R] (I : Ideal R) (h : ∀ (J : Ideal R) (x : J.IsMaximal), Ideal.map (algebraMap R (Localization.AtPrime J)) I = ⊥) : I = ⊥
• Ideal.eq_of_localization_maximal 📋 Mathlib.RingTheory.LocalProperties.Basic
  {R : Type u_1} [CommSemiring R] {I J : Ideal R} (h : ∀ (P : Ideal R) (x : P.IsMaximal), Ideal.map (algebraMap R (Localization.AtPrime P)) I = Ideal.map (algebraMap R (Localization.AtPrime P)) J) : I = J
• Ideal.mem_of_localization_maximal 📋 Mathlib.RingTheory.LocalProperties.Basic
  {R : Type u_1} [CommSemiring R] {r : R} {J : Ideal R} (h : ∀ (P : Ideal R) (x : P.IsMaximal), (algebraMap R (Localization.AtPrime P)) r ∈ Ideal.map (algebraMap R (Localization.AtPrime P)) J) : r ∈ J
• Ideal.le_of_localization_maximal 📋 Mathlib.RingTheory.LocalProperties.Basic
  {R : Type u_1} [CommSemiring R] {I J : Ideal R} (h : ∀ (P : Ideal R) (x : P.IsMaximal), Ideal.map (algebraMap R (Localization.AtPrime P)) I ≤ Ideal.map (algebraMap R (Localization.AtPrime P)) J) : I ≤ J
• Algebra.idealMap_eq_ofEq_comp_toLocalized₀ 📋 Mathlib.RingTheory.LocalProperties.Basic
  {R : Type u_1} (S : Type u_2) [CommSemiring R] [CommSemiring S] [Algebra R S] (p : Submonoid R) [IsLocalization p S] (I : Ideal R) : Algebra.idealMap S I = ↑(LinearEquiv.ofEq (Submodule.localized₀ p (Algebra.linearMap R S) I) (Submodule.restrictScalars R (Ideal.map (algebraMap R S) I)) ⋯) ∘ₗ Submodule.toLocalized₀ p (Algebra.linearMap R S) I
• Ideal.map_eq_top_iff 📋 Mathlib.RingTheory.Ideal.GoingUp
  {R : Type u_3} {S : Type u_4} [CommRing R] [CommRing S] (f : R →+* S) {I : Ideal R} (hf₁ : Function.Injective ⇑f) (hf₂ : f.IsIntegral) : Ideal.map f I = ⊤ ↔ I = ⊤
• Ideal.map_eq_top_iff_of_ker_le 📋 Mathlib.RingTheory.Ideal.GoingUp
  {R : Type u_3} {S : Type u_4} [CommRing R] [CommRing S] (f : R →+* S) {I : Ideal R} (hf₁ : RingHom.ker f ≤ I) (hf₂ : f.IsIntegral) : Ideal.map f I = ⊤ ↔ I = ⊤
• Ideal.injective_quotient_le_comap_map 📋 Mathlib.RingTheory.Ideal.GoingUp
  {R : Type u_1} [CommRing R] (P : Ideal (Polynomial R)) : Function.Injective ⇑(Ideal.quotientMap (Ideal.map (Polynomial.mapRingHom (Ideal.Quotient.mk (Ideal.comap Polynomial.C P))) P) (Polynomial.mapRingHom (Ideal.Quotient.mk (Ideal.comap Polynomial.C P))) ⋯)
• Ideal.quotient_mk_maps_eq 📋 Mathlib.RingTheory.Ideal.GoingUp
  {R : Type u_1} [CommRing R] (P : Ideal (Polynomial R)) : ((Ideal.Quotient.mk (Ideal.map (Polynomial.mapRingHom (Ideal.Quotient.mk (Ideal.comap Polynomial.C P))) P)).comp Polynomial.C).comp (Ideal.Quotient.mk (Ideal.comap Polynomial.C P)) = (Ideal.quotientMap (Ideal.map (Polynomial.mapRingHom (Ideal.Quotient.mk (Ideal.comap Polynomial.C P))) P) (Polynomial.mapRingHom (Ideal.Quotient.mk (Ideal.comap Polynomial.C P))) ⋯).comp ((Ideal.Quotient.mk P).comp Polynomial.C)
• PrimeSpectrum.mem_range_comap_iff 📋 Mathlib.RingTheory.Spectrum.Prime.RingHom
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] (f : R →+* S) {p : PrimeSpectrum R} : p ∈ Set.range f.specComap ↔ Ideal.comap f (Ideal.map f p.asIdeal) = p.asIdeal
• Algebra.TensorProduct.quotIdealMapEquivTensorQuot 📋 Mathlib.RingTheory.TensorProduct.Quotient
  {A : Type u_1} (B : Type u_2) [CommRing A] [CommRing B] [Algebra A B] (I : Ideal A) : (B ⧸ Ideal.map (algebraMap A B) I) ≃ₐ[B] TensorProduct A B (A ⧸ I)
• Algebra.TensorProduct.quotIdealMapEquivTensorQuot_symm_tmul 📋 Mathlib.RingTheory.TensorProduct.Quotient
  {A : Type u_1} (B : Type u_2) [CommRing A] [CommRing B] [Algebra A B] (I : Ideal A) (b : B) (a : A) : (Algebra.TensorProduct.quotIdealMapEquivTensorQuot B I).symm (b ⊗ₜ[A] (Ideal.Quotient.mk I) a) = Submodule.Quotient.mk (a • b)
• Algebra.TensorProduct.quotIdealMapEquivTensorQuot_mk 📋 Mathlib.RingTheory.TensorProduct.Quotient
  {A : Type u_1} (B : Type u_2) [CommRing A] [CommRing B] [Algebra A B] (I : Ideal A) (b : B) : (Algebra.TensorProduct.quotIdealMapEquivTensorQuot B I) ((Ideal.Quotient.mk (Ideal.map (algebraMap A B) I)) b) = b ⊗ₜ[A] 1
• Ideal.comap_map_eq_self_of_faithfullyFlat 📋 Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
  {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] [Module.FaithfullyFlat A B] (I : Ideal A) : Ideal.comap (algebraMap A B) (Ideal.map (algebraMap A B) I) = I

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.

This is Loogle revision 19971e9 serving mathlib revision 40fea08