Loogle!

Result

Found 550 declarations mentioning Ideal.IsPrime. Of these, only the first 200 are shown.

• Ideal.IsPrime 📋 Mathlib.RingTheory.Ideal.Prime
  {α : Type u} [Semiring α] (I : Ideal α) : Prop
• Ideal.primeCompl 📋 Mathlib.RingTheory.Ideal.Prime
  {α : Type u} [Semiring α] (P : Ideal α) [hp : P.IsPrime] : Submonoid α
• Ideal.IsPrime.ne_top 📋 Mathlib.RingTheory.Ideal.Prime
  {α : Type u} [Semiring α] {I : Ideal α} (hI : I.IsPrime) : I ≠ ⊤
• Ideal.IsPrime.ne_top' 📋 Mathlib.RingTheory.Ideal.Prime
  {α : Type u} {inst✝ : Semiring α} {I : Ideal α} [self : I.IsPrime] : I ≠ ⊤
• IsDomain.of_bot_isPrime 📋 Mathlib.RingTheory.Ideal.Prime
  (A : Type u_1) [Ring A] [hbp : ⊥.IsPrime] : IsDomain A
• Ideal.bot_prime 📋 Mathlib.RingTheory.Ideal.Prime
  {α : Type u} [Semiring α] [Nontrivial α] [NoZeroDivisors α] : ⊥.IsPrime
• Ideal.eq_bot_of_prime 📋 Mathlib.RingTheory.Ideal.Prime
  {K : Type u} [DivisionSemiring K] (I : Ideal K) [h : I.IsPrime] : I = ⊥
• Ideal.one_notMem 📋 Mathlib.RingTheory.Ideal.Prime
  {α : Type u} [Semiring α] (I : Ideal α) [hI : I.IsPrime] : 1 ∉ I
• Ideal.IsPrime.one_notMem 📋 Mathlib.RingTheory.Ideal.Prime
  {α : Type u} [Semiring α] {I : Ideal α} (hI : I.IsPrime) : 1 ∉ I
• Ideal.mem_primeCompl_iff 📋 Mathlib.RingTheory.Ideal.Prime
  {α : Type u} [Semiring α] {P : Ideal α} [P.IsPrime] {x : α} : x ∈ P.primeCompl ↔ x ∉ P
• Ideal.IsPrime.mem_of_pow_mem 📋 Mathlib.RingTheory.Ideal.Prime
  {α : Type u} [Semiring α] {I : Ideal α} (hI : I.IsPrime) {r : α} (n : ℕ) (H : r ^ n ∈ I) : r ∈ I
• Ideal.IsPrime.pow_mem_iff_mem 📋 Mathlib.RingTheory.Ideal.Prime
  {α : Type u} [Semiring α] {I : Ideal α} (hI : I.IsPrime) {r : α} (n : ℕ) (hn : 0 < n) : r ^ n ∈ I ↔ r ∈ I
• Ideal.IsPrime.mem_or_mem_of_mul_eq_zero 📋 Mathlib.RingTheory.Ideal.Prime
  {α : Type u} [Semiring α] {I : Ideal α} (hI : I.IsPrime) {x y : α} (h : x * y = 0) : x ∈ I ∨ y ∈ I
• Ideal.IsPrime.mem_or_mem 📋 Mathlib.RingTheory.Ideal.Prime
  {α : Type u} [Semiring α] {I : Ideal α} (hI : I.IsPrime) {x y : α} : x * y ∈ I → x ∈ I ∨ y ∈ I
• Ideal.IsPrime.mem_or_mem' 📋 Mathlib.RingTheory.Ideal.Prime
  {α : Type u} {inst✝ : Semiring α} {I : Ideal α} [self : I.IsPrime] {x y : α} : x * y ∈ I → x ∈ I ∨ y ∈ I
• Ideal.IsPrime.mul_notMem 📋 Mathlib.RingTheory.Ideal.Prime
  {α : Type u} [Semiring α] {I : Ideal α} (hI : I.IsPrime) {x y : α} : x ∉ I → y ∉ I → x * y ∉ I
• Ideal.IsPrime.mul_mem_iff_mem_or_mem 📋 Mathlib.RingTheory.Ideal.Prime
  {α : Type u} [Semiring α] {I : Ideal α} [I.IsTwoSided] (hI : I.IsPrime) {x y : α} : x * y ∈ I ↔ x ∈ I ∨ y ∈ I
• Ideal.IsPrime.mul_mem_left_iff 📋 Mathlib.RingTheory.Ideal.Prime
  {α : Type u} [Semiring α] {I : Ideal α} [I.IsTwoSided] [I.IsPrime] {x y : α} (hx : x ∉ I) : x * y ∈ I ↔ y ∈ I
• Ideal.IsPrime.mul_mem_right_iff 📋 Mathlib.RingTheory.Ideal.Prime
  {α : Type u} [Semiring α] {I : Ideal α} [I.IsTwoSided] [I.IsPrime] {x y : α} (hx : y ∉ I) : x * y ∈ I ↔ x ∈ I
• Ideal.IsPrime.mk 📋 Mathlib.RingTheory.Ideal.Prime
  {α : Type u} [Semiring α] {I : Ideal α} (ne_top' : I ≠ ⊤) (mem_or_mem' : ∀ {x y : α}, x * y ∈ I → x ∈ I ∨ y ∈ I) : I.IsPrime
• Ideal.isPrime_iff 📋 Mathlib.RingTheory.Ideal.Prime
  {α : Type u} [Semiring α] {I : Ideal α} : I.IsPrime ↔ I ≠ ⊤ ∧ ∀ {x y : α}, x * y ∈ I → x ∈ I ∨ y ∈ I
• Ideal.not_isPrime_iff 📋 Mathlib.RingTheory.Ideal.Prime
  {α : Type u} [Semiring α] {I : Ideal α} : ¬I.IsPrime ↔ I = ⊤ ∨ ∃ x, ∃ (_ : x ∉ I), ∃ y, ∃ (_ : y ∉ I), x * y ∈ I
• Ideal.IsMaximal.isPrime 📋 Mathlib.RingTheory.Ideal.Maximal
  {α : Type u} [CommSemiring α] {I : Ideal α} (H : I.IsMaximal) : I.IsPrime
• Ideal.IsMaximal.isPrime' 📋 Mathlib.RingTheory.Ideal.Maximal
  {α : Type u} [CommSemiring α] (I : Ideal α) [_H : I.IsMaximal] : I.IsPrime
• Ideal.span_singleton_prime 📋 Mathlib.RingTheory.Ideal.Maximal
  {α : Type u} [CommSemiring α] {p : α} (hp : p ≠ 0) : (Ideal.span {p}).IsPrime ↔ Prime p
• Ideal.isPrime_iff_of_isPrincipalIdealRing 📋 Mathlib.RingTheory.Ideal.Maximal
  {α : Type u} [CommSemiring α] [IsPrincipalIdealRing α] {P : Ideal α} (hP : P ≠ ⊥) : P.IsPrime ↔ ∃ p, Prime p ∧ P = Ideal.span {p}
• Ideal.sInf_isPrime_of_isChain 📋 Mathlib.RingTheory.Ideal.Maximal
  {α : Type u} [Semiring α] {s : Set (Ideal α)} (hs : s.Nonempty) (hs' : IsChain (fun x1 x2 => x1 ≤ x2) s) (H : ∀ p ∈ s, p.IsPrime) : (sInf s).IsPrime
• Ideal.isPrime_iff_of_isPrincipalIdealRing_of_noZeroDivisors 📋 Mathlib.RingTheory.Ideal.Maximal
  {α : Type u} [CommSemiring α] [IsPrincipalIdealRing α] [NoZeroDivisors α] [Nontrivial α] {P : Ideal α} : P.IsPrime ↔ P = ⊥ ∨ ∃ p, Prime p ∧ P = Ideal.span {p}
• Ideal.exists_le_prime_notMem_of_isIdempotentElem 📋 Mathlib.RingTheory.Ideal.Maximal
  {α : Type u} [CommSemiring α] (I : Ideal α) (a : α) (ha : IsIdempotentElem a) (haI : a ∉ I) : ∃ p, p.IsPrime ∧ I ≤ p ∧ a ∉ p
• Ideal.isPrime_of_maximally_disjoint 📋 Mathlib.RingTheory.Ideal.Maximal
  {α : Type u} [CommSemiring α] (I : Ideal α) (S : Submonoid α) (disjoint : Disjoint ↑I ↑S) (maximally_disjoint : ∀ (J : Ideal α), I < J → ¬Disjoint ↑J ↑S) : I.IsPrime
• Ideal.exists_le_prime_disjoint 📋 Mathlib.RingTheory.Ideal.Maximal
  {α : Type u} [CommSemiring α] (I : Ideal α) (S : Submonoid α) (disjoint : Disjoint ↑I ↑S) : ∃ p, p.IsPrime ∧ I ≤ p ∧ Disjoint ↑p ↑S
• Ring.not_isField_iff_exists_prime 📋 Mathlib.RingTheory.Ideal.Basic
  {R : Type u_5} [CommSemiring R] [Nontrivial R] : ¬IsField R ↔ ∃ p, p ≠ ⊥ ∧ p.IsPrime
• Ideal.Quotient.isDomain 📋 Mathlib.RingTheory.Ideal.Quotient.Basic
  {R : Type u_3} [Ring R] (I : Ideal R) [I.IsTwoSided] [hI : I.IsPrime] : IsDomain (R ⧸ I)
• Ideal.Quotient.isDomain_iff_prime 📋 Mathlib.RingTheory.Ideal.Quotient.Basic
  {R : Type u_3} [Ring R] (I : Ideal R) [I.IsTwoSided] : IsDomain (R ⧸ I) ↔ I.IsPrime
• Ideal.Quotient.noZeroDivisors 📋 Mathlib.RingTheory.Ideal.Quotient.Basic
  {R : Type u_3} [Ring R] (I : Ideal R) [I.IsTwoSided] [hI : I.IsPrime] : NoZeroDivisors (R ⧸ I)
• Ideal.IsPrime.isRadical 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u} [CommSemiring R] {I : Ideal R} (H : I.IsPrime) : I.IsRadical
• Ideal.IsPrime.radical 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u} [CommSemiring R] {I : Ideal R} (H : I.IsPrime) : I.radical = I
• Ideal.IsPrime.notMem_of_isCoprime_of_mem 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u} [CommSemiring R] {I : Ideal R} [I.IsPrime] {x y : R} (h : IsCoprime x y) (hx : x ∈ I) : y ∉ I
• Ideal.IsPrime.multiset_prod_mem_iff_exists_mem 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u} [CommSemiring R] {I : Ideal R} (hI : I.IsPrime) (s : Multiset R) : s.prod ∈ I ↔ ∃ p ∈ s, p ∈ I
• Ideal.IsPrime.prod_mem_iff_exists_mem 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u} [CommSemiring R] {I : Ideal R} (hI : I.IsPrime) (s : Finset R) : ∏ x ∈ s, x ∈ I ↔ ∃ p ∈ s, p ∈ I
• Ideal.radical_eq_sInf 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u} [CommSemiring R] (I : Ideal R) : I.radical = sInf {J | I ≤ J ∧ J.IsPrime}
• Ideal.IsPrime.prod_mem_iff 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u} {ι : Type u_1} [CommSemiring R] {s : Finset ι} {x : ι → R} {p : Ideal R} [hp : p.IsPrime] : ∏ i ∈ s, x i ∈ p ↔ ∃ i ∈ s, x i ∈ p
• Ideal.primeCompl_le_nonZeroDivisors 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u_1} [CommSemiring R] [NoZeroDivisors R] (P : Ideal R) [P.IsPrime] : P.primeCompl ≤ nonZeroDivisors R
• Ideal.IsPrime.radical_le_iff 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u} [CommSemiring R] {I J : Ideal R} (hJ : J.IsPrime) : I.radical ≤ J ↔ I ≤ J
• Ideal.coprime_of_no_prime_ge 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u} [CommSemiring R] {I J : Ideal R} (h : ∀ (P : Ideal R), I ≤ P → J ≤ P → ¬P.IsPrime) : IsCoprime I J
• Ideal.IsPrime.prod_le 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u} {ι : Type u_1} [CommSemiring R] {s : Finset ι} {f : ι → Ideal R} {P : Ideal R} (hp : P.IsPrime) : s.prod f ≤ P ↔ ∃ i ∈ s, f i ≤ P
• Ideal.IsPrime.le_of_pow_le 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u} [CommSemiring R] {I P : Ideal R} [hP : P.IsPrime] {n : ℕ} (h : I ^ n ≤ P) : I ≤ P
• Ideal.IsPrime.multiset_prod_map_le 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u} {ι : Type u_1} [CommSemiring R] {s : Multiset ι} (f : ι → Ideal R) {P : Ideal R} (hp : P.IsPrime) : (Multiset.map f s).prod ≤ P ↔ ∃ i ∈ s, f i ≤ P
• Ideal.IsPrime.pow_le_iff 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u} [CommSemiring R] {I P : Ideal R} [hP : P.IsPrime] {n : ℕ} (hn : n ≠ 0) : I ^ n ≤ P ↔ I ≤ P
• Ideal.IsPrime.multiset_prod_le 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u} [CommSemiring R] {s : Multiset (Ideal R)} {P : Ideal R} (hp : P.IsPrime) : s.prod ≤ P ↔ ∃ I ∈ s, I ≤ P
• Ideal.IsPrime.inf_le' 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u} {ι : Type u_1} [CommSemiring R] {s : Finset ι} {f : ι → Ideal R} {P : Ideal R} (hp : P.IsPrime) : s.inf f ≤ P ↔ ∃ i ∈ s, f i ≤ P
• Ideal.IsPrime.inf_le 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u} [CommSemiring R] {I J P : Ideal R} (hp : P.IsPrime) : I ⊓ J ≤ P ↔ I ≤ P ∨ J ≤ P
• Ideal.IsPrime.mul_le 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u} [CommSemiring R] {I J P : Ideal R} (hp : P.IsPrime) : I * J ≤ P ↔ I ≤ P ∨ J ≤ P
• Ideal.subset_union_prime_finite 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u_2} {ι : Type u_3} [CommRing R] {s : Set ι} (hs : s.Finite) {f : ι → Ideal R} (a b : ι) (hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime) {I : Ideal R} : ↑I ⊆ ⋃ i ∈ s, ↑(f i) ↔ ∃ i ∈ s, I ≤ f i
• Ideal.subset_union_prime 📋 Mathlib.RingTheory.Ideal.Operations
  {ι : Type u_1} {R : Type u} [CommRing R] {s : Finset ι} {f : ι → Ideal R} (a b : ι) (hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime) {I : Ideal R} : ↑I ⊆ ⋃ i ∈ ↑s, ↑(f i) ↔ ∃ i ∈ s, I ≤ f i
• Ideal.subset_union_prime' 📋 Mathlib.RingTheory.Ideal.Operations
  {ι : Type u_1} {R : Type u} [CommRing R] {s : Finset ι} {f : ι → Ideal R} {a b : ι} (hp : ∀ i ∈ s, (f i).IsPrime) {I : Ideal R} : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i) ↔ I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
• RingHom.ker_isPrime 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [IsDomain S] [FunLike F R S] [RingHomClass F R S] (f : F) : (RingHom.ker f).IsPrime
• Ideal.comap_isPrime 📋 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] [H : K.IsPrime] : (Ideal.comap f K).IsPrime
• Ideal.IsPrime.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] [hK : K.IsPrime] : (Ideal.comap f K).IsPrime
• 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.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_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.exists_ideal_comap_le_prime 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {F : Type u_1} [Semiring R] {S : Type u_2} [CommSemiring S] [FunLike F R S] [RingHomClass F R S] {f : F} (P : Ideal R) [P.IsPrime] (I : Ideal S) (le : Ideal.comap f I ≤ P) : ∃ Q ≥ I, Q.IsPrime ∧ Ideal.comap f Q ≤ P
• Ideal.disjoint_map_primeCompl_iff_comap_le 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} [CommSemiring R] {S : Type u_2} [Semiring S] {f : R →+* S} {p : Ideal R} {I : Ideal S} [p.IsPrime] : Disjoint ↑I ↑(Submonoid.map f p.primeCompl) ↔ Ideal.comap f I ≤ p
• Ideal.isPrime_ideal_prod_top 📋 Mathlib.RingTheory.Ideal.Prod
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {I : Ideal R} [h : I.IsPrime] : (I.prod ⊤).IsPrime
• Ideal.isPrime_ideal_prod_top' 📋 Mathlib.RingTheory.Ideal.Prod
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {I : Ideal S} [h : I.IsPrime] : (⊤.prod I).IsPrime
• Ideal.isPrime_of_isPrime_prod_top 📋 Mathlib.RingTheory.Ideal.Prod
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {I : Ideal R} (h : (I.prod ⊤).IsPrime) : I.IsPrime
• Ideal.isPrime_of_isPrime_prod_top' 📋 Mathlib.RingTheory.Ideal.Prod
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {I : Ideal S} (h : (⊤.prod I).IsPrime) : I.IsPrime
• Ideal.ideal_prod_prime_aux 📋 Mathlib.RingTheory.Ideal.Prod
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {I : Ideal R} {J : Ideal S} : (I.prod J).IsPrime → I = ⊤ ∨ J = ⊤
• Ideal.ideal_prod_prime 📋 Mathlib.RingTheory.Ideal.Prod
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (I : Ideal (R × S)) : I.IsPrime ↔ (∃ p, p.IsPrime ∧ I = p.prod ⊤) ∨ ∃ p, p.IsPrime ∧ I = ⊤.prod p
• Ideal.IsPrime.exists_mem_prime_of_ne_bot 📋 Mathlib.RingTheory.UniqueFactorizationDomain.Ideal
  {R : Type u_2} [CommSemiring R] [IsDomain R] [UniqueFactorizationMonoid R] {I : Ideal R} (hI₂ : I.IsPrime) (hI : I ≠ ⊥) : ∃ x ∈ I, Prime x
• IsPrime.to_maximal_ideal 📋 Mathlib.RingTheory.PrincipalIdealDomain
  {R : Type u} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {S : Ideal R} [hpi : S.IsPrime] (hS : S ≠ ⊥) : S.IsMaximal
• Submodule.IsPrincipal.prime_generator_of_isPrime 📋 Mathlib.RingTheory.PrincipalIdealDomain
  {R : Type u} [CommSemiring R] (S : Ideal R) [Submodule.IsPrincipal S] [is_prime : S.IsPrime] (ne_bot : S ≠ ⊥) : Prime (Submodule.IsPrincipal.generator S)
• Ideal.isPrime_map_C_of_isPrime 📋 Mathlib.RingTheory.Polynomial.Basic
  {R : Type u} [CommRing R] {P : Ideal R} [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.isPrime_map_quotientMk_of_isPrime 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  {R : Type u} [Ring R] {I : Ideal R} [I.IsTwoSided] {p : Ideal R} [p.IsPrime] (hIP : I ≤ p) : (Ideal.map (Ideal.Quotient.mk I) p).IsPrime
• Ideal.IsPrime.isPrimary 📋 Mathlib.RingTheory.Ideal.IsPrimary
  {R : Type u_1} [CommSemiring R] {I : Ideal R} (hi : I.IsPrime) : I.IsPrimary
• Ideal.isPrime_radical 📋 Mathlib.RingTheory.Ideal.IsPrimary
  {R : Type u_1} [CommSemiring R] {I : Ideal R} (hi : I.IsPrimary) : I.radical.IsPrime
• IsLocalRing.of_unique_nonzero_prime 📋 Mathlib.RingTheory.LocalRing.Basic
  {R : Type u_1} [CommSemiring R] (h : ∃! P, P ≠ ⊥ ∧ P.IsPrime) : IsLocalRing R
• IsLocalRing.le_maximalIdeal_of_isPrime 📋 Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
  {R : Type u_1} [CommSemiring R] [IsLocalRing R] (p : Ideal R) [hp : p.IsPrime] : p ≤ IsLocalRing.maximalIdeal R
• Ideal.IsPrime.smul 📋 Mathlib.RingTheory.Ideal.Pointwise
  {M : Type u_1} {R : Type u_2} [Group M] [Semiring R] [MulSemiringAction M R] {I : Ideal R} [H : I.IsPrime] (g : M) : (g • I).IsPrime
• Ideal.IsPrime.smul_iff 📋 Mathlib.RingTheory.Ideal.Pointwise
  {M : Type u_1} {R : Type u_2} [Group M] [Semiring R] [MulSemiringAction M R] {I : Ideal R} (g : M) : (g • I).IsPrime ↔ I.IsPrime
• Ideal.IsPrime.under 📋 Mathlib.RingTheory.Ideal.Over
  (A : Type u_2) [CommSemiring A] {B : Type u_3} [Semiring B] [Algebra A B] (P : Ideal B) [hP : P.IsPrime] : (Ideal.under A P).IsPrime
• Ideal.primesOver.mk 📋 Mathlib.RingTheory.Ideal.Over
  {A : Type u_2} [CommSemiring A] (p : Ideal A) {B : Type u_3} [Semiring B] [Algebra A B] (P : Ideal B) [hPp : P.IsPrime] [hp : P.LiesOver p] : ↑(p.primesOver B)
• Ideal.primesOver.isPrime 📋 Mathlib.RingTheory.Ideal.Over
  {A : Type u_2} [CommSemiring A] (p : Ideal A) {B : Type u_3} [Semiring B] [Algebra A B] (Q : ↑(p.primesOver B)) : (↑Q).IsPrime
• Ideal.Quotient.nontrivial_of_liesOver_of_isPrime 📋 Mathlib.RingTheory.Ideal.Over
  {A : Type u_3} {B : Type u_4} [CommRing A] [CommRing B] [Algebra A B] (P : Ideal B) (p : Ideal A) [P.LiesOver p] [hp : p.IsPrime] : Nontrivial (B ⧸ P)
• Ideal.primeCompl.eq_1 📋 Mathlib.RingTheory.Ideal.Over
  {α : Type u} [Semiring α] (P : Ideal α) [hp : P.IsPrime] : P.primeCompl = { carrier := (↑P)ᶜ, mul_mem' := ⋯, one_mem' := ⋯ }
• Ideal.disjoint_primeCompl_of_liesOver 📋 Mathlib.RingTheory.Ideal.Over
  {A : Type u_2} [CommSemiring A] {C : Type u_4} [Semiring C] [Algebra A C] (𝔓 : Ideal C) (p : Ideal A) [p.IsPrime] [hPp : 𝔓.LiesOver p] : Disjoint ↑(Algebra.algebraMapSubmonoid C p.primeCompl) ↑𝔓
• Ideal.Quotient.instIsPrimeQuotientMapRingHomAlgebraMapMkOfLiesOver 📋 Mathlib.RingTheory.Ideal.Over
  (R : Type u_2) [CommSemiring R] {A : Type u_3} [CommRing A] [Algebra R A] (p : Ideal R) (P : Ideal A) [P.IsPrime] [P.LiesOver p] : (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R A) p)) P).IsPrime
• PrimeSpectrum.isPrime 📋 Mathlib.RingTheory.Spectrum.Prime.Defs
  {R : Type u_1} [CommSemiring R] (self : PrimeSpectrum R) : self.asIdeal.IsPrime
• PrimeSpectrum.mk 📋 Mathlib.RingTheory.Spectrum.Prime.Defs
  {R : Type u_1} [CommSemiring R] (asIdeal : Ideal R) (isPrime : asIdeal.IsPrime) : PrimeSpectrum R
• PrimeSpectrum.mk.injEq 📋 Mathlib.RingTheory.Spectrum.Prime.Defs
  {R : Type u_1} [CommSemiring R] (asIdeal : Ideal R) (isPrime : asIdeal.IsPrime) (asIdeal✝ : Ideal R) (isPrime✝ : asIdeal✝.IsPrime) : ({ asIdeal := asIdeal, isPrime := isPrime } = { asIdeal := asIdeal✝, isPrime := isPrime✝ }) = (asIdeal = asIdeal✝)
• PrimeSpectrum.mk.sizeOf_spec 📋 Mathlib.RingTheory.Spectrum.Prime.Defs
  {R : Type u_1} [CommSemiring R] [SizeOf R] (asIdeal : Ideal R) (isPrime : asIdeal.IsPrime) : sizeOf { asIdeal := asIdeal, isPrime := isPrime } = 1 + sizeOf asIdeal + sizeOf isPrime
• PrimeSpectrum.equivSubtype 📋 Mathlib.RingTheory.Spectrum.Prime.Defs
  (R : Type u_1) [CommSemiring R] : PrimeSpectrum R ≃o { I // I.IsPrime }
• PrimeSpectrum.equivSubtype_apply_coe 📋 Mathlib.RingTheory.Spectrum.Prime.Defs
  (R : Type u_1) [CommSemiring R] (I : PrimeSpectrum R) : ↑((PrimeSpectrum.equivSubtype R) I) = I.asIdeal
• PrimeSpectrum.equivSubtype_symm_apply_asIdeal 📋 Mathlib.RingTheory.Spectrum.Prime.Defs
  (R : Type u_1) [CommSemiring R] (I : { I // I.IsPrime }) : ((RelIso.symm (PrimeSpectrum.equivSubtype R)) I).asIdeal = ↑I
• IsLocalization.instIsDomainLocalizationAlgebraMapSubmonoidPrimeComplOfFaithfulSMul 📋 Mathlib.RingTheory.Localization.Ideal
  {R : Type u_1} [CommRing R] (S : Type u_2) [CommRing S] [Algebra R S] {P : Ideal R} [P.IsPrime] [IsDomain R] [IsDomain S] [FaithfulSMul R S] : IsDomain (Localization (Algebra.algebraMapSubmonoid S P.primeCompl))
• 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.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.isPrime_iff_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] (J : Ideal S) : J.IsPrime ↔ (Ideal.comap (algebraMap R S) J).IsPrime ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) J)
• IsLocalization.orderIsoOfPrime 📋 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] : { p // p.IsPrime } ≃o { p // p.IsPrime ∧ Disjoint ↑M ↑p }
• IsLocalization.bot_lt_comap_prime 📋 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] [IsDomain R] (hM : M ≤ nonZeroDivisors R) (p : Ideal S) [hpp : p.IsPrime] (hp0 : p ≠ ⊥) : ⊥ < Ideal.comap (algebraMap R S) p
• IsLocalization.surjective_quotientMap_of_maximal_of_localization 📋 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] {I : Ideal S} [I.IsPrime] {J : Ideal R} {H : J ≤ Ideal.comap (algebraMap R S) I} (hI : (Ideal.comap (algebraMap R S) I).IsMaximal) : Function.Surjective ⇑(Ideal.quotientMap I (algebraMap R S) H)
• IsLocalization.orderIsoOfPrime_apply_coe 📋 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] (p : { p // p.IsPrime }) : ↑((IsLocalization.orderIsoOfPrime M S) p) = Ideal.comap (algebraMap R S) ↑p
• IsLocalization.orderIsoOfPrime_symm_apply_coe 📋 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] (p : { p // p.IsPrime ∧ Disjoint ↑M ↑p }) : ↑((RelIso.symm (IsLocalization.orderIsoOfPrime M S)) p) = Ideal.map (algebraMap R S) ↑p
• Ideal.minimalPrimes_isPrime 📋 Mathlib.RingTheory.Ideal.MinimalPrime.Basic
  {R : Type u_1} [CommSemiring R] {I p : Ideal R} (h : p ∈ I.minimalPrimes) : p.IsPrime
• Ideal.minimalPrimes_eq_subsingleton_self 📋 Mathlib.RingTheory.Ideal.MinimalPrime.Basic
  {R : Type u_1} [CommRing R] {I : Ideal R} [I.IsPrime] : I.minimalPrimes = {I}
• minimalPrimes_eq_minimals 📋 Mathlib.RingTheory.Ideal.MinimalPrime.Basic
  {R : Type u_1} [CommSemiring R] : minimalPrimes R = {x | Minimal Ideal.IsPrime x}
• Ideal.minimalPrimes.eq_1 📋 Mathlib.RingTheory.Ideal.MinimalPrime.Basic
  {R : Type u_1} [CommSemiring R] (I : Ideal R) : I.minimalPrimes = {p | Minimal (fun q => q.IsPrime ∧ I ≤ q) p}
• Ideal.exists_minimalPrimes_le 📋 Mathlib.RingTheory.Ideal.MinimalPrime.Basic
  {R : Type u_1} [CommSemiring R] {I J : Ideal R} [J.IsPrime] (e : I ≤ J) : ∃ p ∈ I.minimalPrimes, p ≤ J
• Ideal.map_sup_mem_minimalPrimes_of_map_quotientMk_mem_minimalPrimes 📋 Mathlib.RingTheory.Ideal.MinimalPrime.Basic
  {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommRing S] [Algebra R S] {I p : Ideal R} {P : Ideal S} [P.IsPrime] [P.LiesOver p] (hI : p ∈ I.minimalPrimes) {J : Ideal S} (hJP : J ≤ P) (hJ : Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) P ∈ (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) J).minimalPrimes) : P ∈ (Ideal.map (algebraMap R S) I ⊔ J).minimalPrimes
• Localization.AtPrime 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
  {R : Type u_1} [CommSemiring R] (P : Ideal R) [hp : P.IsPrime] : Type u_1
• IsLocalization.AtPrime 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
  {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (P : Ideal R) [hp : P.IsPrime] : Prop
• IsLocalization.AtPrime.Nontrivial 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
  {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (P : Ideal R) [hp : P.IsPrime] [IsLocalization.AtPrime S P] : Nontrivial S
• IsLocalization.AtPrime.nontrivial 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
  {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (P : Ideal R) [hp : P.IsPrime] [IsLocalization.AtPrime S P] : Nontrivial S
• IsLocalization.AtPrime.isLocalRing 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
  {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (P : Ideal R) [hp : P.IsPrime] [IsLocalization.AtPrime S P] : IsLocalRing S
• Localization.AtPrime.isLocalRing 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
  {R : Type u_1} [CommSemiring R] (P : Ideal R) [hp : P.IsPrime] : IsLocalRing (Localization P.primeCompl)
• IsLocalization.isDomain_of_atPrime 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
  {A : Type u_4} [CommRing A] [IsDomain A] (S : Type u_5) [CommSemiring S] [Algebra A S] (P : Ideal A) [P.IsPrime] [IsLocalization.AtPrime S P] : IsDomain S
• Ideal.primeCompl.congr_simp 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
  {α : Type u} [Semiring α] (P P✝ : Ideal α) (e_P : P = P✝) [hp : P.IsPrime] : P.primeCompl = P✝.primeCompl
• Localization.AtPrime.congr_simp 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
  {R : Type u_1} [CommSemiring R] (P P✝ : Ideal R) (e_P : P = P✝) [hp : P.IsPrime] : Localization.AtPrime P = Localization.AtPrime P✝
• IsLocalization.AtPrime.liesOver_maximalIdeal 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
  {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (I : Ideal R) [hI : I.IsPrime] [IsLocalization.AtPrime S I] (h : IsLocalRing S := ⋯) : (IsLocalRing.maximalIdeal S).LiesOver I
• IsLocalization.isDomain_of_local_atPrime 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
  {A : Type u_4} [CommRing A] [IsDomain A] {P : Ideal A} (x✝ : P.IsPrime) : IsDomain (Localization.AtPrime P)
• IsLocalization.AtPrime.congr_simp 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
  {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (P P✝ : Ideal R) (e_P : P = P✝) [hp : P.IsPrime] : IsLocalization.AtPrime S P = IsLocalization.AtPrime S P✝
• IsLocalization.AtPrime.faithfulSMul 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
  (S : Type u_2) [CommSemiring S] (R : Type u_4) [CommRing R] [NoZeroDivisors R] [Algebra R S] (P : Ideal R) [hp : P.IsPrime] [IsLocalization.AtPrime S P] : FaithfulSMul R S
• IsLocalization.AtPrime.isMaximal_map 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
  {R : Type u_1} [CommSemiring R] (p : Ideal R) [p.IsPrime] (Rₚ : Type u_4) [CommSemiring Rₚ] [Algebra R Rₚ] [IsLocalization.AtPrime Rₚ p] [IsLocalRing Rₚ] : (Ideal.map (algebraMap R Rₚ) p).IsMaximal
• IsLocalization.AtPrime.map_eq_maximalIdeal 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
  {R : Type u_1} [CommSemiring R] (p : Ideal R) [p.IsPrime] (Rₚ : Type u_4) [CommSemiring Rₚ] [Algebra R Rₚ] [IsLocalization.AtPrime Rₚ p] [IsLocalRing Rₚ] : Ideal.map (algebraMap R Rₚ) p = IsLocalRing.maximalIdeal Rₚ
• IsLocalization.AtPrime.comap_maximalIdeal 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
  {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (I : Ideal R) [hI : I.IsPrime] [IsLocalization.AtPrime S I] (h : IsLocalRing S := ⋯) : Ideal.comap (algebraMap R S) (IsLocalRing.maximalIdeal S) = I
• IsLocalization.AtPrime.primeSpectrumOrderIso 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
  {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (I : Ideal R) [hI : I.IsPrime] [IsLocalization.AtPrime S I] : PrimeSpectrum S ≃o ↑(Set.Iic { asIdeal := I, isPrime := hI })
• IsLocalization.AtPrime.isPrime_map_of_liesOver 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
  {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (p : Ideal R) [p.IsPrime] (Sₚ : Type u_5) [CommSemiring Sₚ] [Algebra S Sₚ] [IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ] (P : Ideal S) [P.IsPrime] [P.LiesOver p] : (Ideal.map (algebraMap S Sₚ) P).IsPrime
• IsLocalization.AtPrime.isUnit_to_map_iff 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
  {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (I : Ideal R) [hI : I.IsPrime] [IsLocalization.AtPrime S I] (x : R) : IsUnit ((algebraMap R S) x) ↔ x ∈ I.primeCompl
• Localization.AtPrime.instAlgebraOfLiesOver 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
  {A : Type u_4} {B : Type u_5} [CommRing A] [CommRing B] [Algebra A B] (p : Ideal A) [p.IsPrime] (P : Ideal B) [P.IsPrime] [P.LiesOver p] : Algebra (Localization.AtPrime p) (Localization.AtPrime P)
• Ideal.isPrime_map_of_isLocalizationAtPrime 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
  {R : Type u_1} [CommSemiring R] (q : Ideal R) [q.IsPrime] {S : Type u_4} [CommSemiring S] [Algebra R S] [IsLocalization.AtPrime S q] {p : Ideal R} [p.IsPrime] (hpq : p ≤ q) : (Ideal.map (algebraMap R S) p).IsPrime
• IsLocalization.AtPrime.isUnit_mk'_iff 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
  {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (I : Ideal R) [hI : I.IsPrime] [IsLocalization.AtPrime S I] (x : R) (y : ↥I.primeCompl) : IsUnit (IsLocalization.mk' S x y) ↔ x ∈ I.primeCompl
• Ideal.under_map_of_isLocalizationAtPrime 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
  {R : Type u_1} [CommSemiring R] (q : Ideal R) [q.IsPrime] {S : Type u_4} [CommSemiring 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.instAlgebraOfLiesOver.congr_simp 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
  {A : Type u_4} {B : Type u_5} [CommRing A] [CommRing B] [Algebra A B] (p : Ideal A) [p.IsPrime] (P : Ideal B) [P.IsPrime] [P.LiesOver p] : Localization.AtPrime.instAlgebraOfLiesOver p P = Localization.AtPrime.instAlgebraOfLiesOver p P
• IsLocalization.AtPrime.to_map_mem_maximal_iff 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
  {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (I : Ideal R) [hI : I.IsPrime] [IsLocalization.AtPrime S I] (x : R) (h : IsLocalRing S := ⋯) : (algebraMap R S) x ∈ IsLocalRing.maximalIdeal S ↔ x ∈ I
• Localization.instFaithfulSMulAtPrimeOfNoZeroDivisors 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
  {R : Type u_4} [CommRing R] [NoZeroDivisors R] (P : Ideal R) [hp : P.IsPrime] : FaithfulSMul R (Localization.AtPrime P)
• Localization.localRingHom 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
  {R : Type u_1} [CommSemiring R] {P : Type u_3} [CommSemiring P] (I : Ideal R) [hI : I.IsPrime] (J : Ideal P) [J.IsPrime] (f : R →+* P) (hIJ : I = Ideal.comap f J) : Localization.AtPrime I →+* Localization.AtPrime J
• IsLocalization.AtPrime.comap_map_of_isMaximal 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
  {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (p : Ideal R) [p.IsPrime] (Sₚ : Type u_5) [CommSemiring Sₚ] [Algebra S Sₚ] [IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ] (P : Ideal S) [P.IsMaximal] [P.LiesOver p] : Ideal.comap (algebraMap S Sₚ) (Ideal.map (algebraMap S Sₚ) P) = P
• IsLocalization.AtPrime.mk'_mem_maximal_iff 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
  {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (I : Ideal R) [hI : I.IsPrime] [IsLocalization.AtPrime S I] (x : R) (y : ↥I.primeCompl) (h : IsLocalRing S := ⋯) : IsLocalization.mk' S x y ∈ IsLocalRing.maximalIdeal S ↔ x ∈ I
• Localization.localRingHom_id 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
  {R : Type u_1} [CommSemiring R] (I : Ideal R) [hI : I.IsPrime] : Localization.localRingHom I I (RingHom.id R) ⋯ = RingHom.id (Localization.AtPrime I)
• Localization.AtPrime.map_eq_maximalIdeal 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
  {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)
• IsLocalization.AtPrime.orderIsoOfPrime 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
  {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (I : Ideal R) [hI : I.IsPrime] [IsLocalization.AtPrime S I] : { p // p.IsPrime } ≃o { p // p.IsPrime ∧ p ≤ I }
• Localization.AtPrime.comap_maximalIdeal 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
  {R : Type u_1} [CommSemiring R] {I : Ideal R} [hI : I.IsPrime] : Ideal.comap (algebraMap R (Localization.AtPrime I)) (IsLocalRing.maximalIdeal (Localization I.primeCompl)) = I
• Localization.localRingHom.congr_simp 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
  {R : Type u_1} [CommSemiring R] {P : Type u_3} [CommSemiring P] (I : Ideal R) [hI : I.IsPrime] (J : Ideal P) [J.IsPrime] (f f✝ : R →+* P) (e_f : f = f✝) (hIJ : I = Ideal.comap f J) : Localization.localRingHom I J f hIJ = Localization.localRingHom I J f✝ ⋯
• Localization.isLocalHom_localRingHom 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
  {R : Type u_1} [CommSemiring R] {P : Type u_3} [CommSemiring P] (I : Ideal R) [hI : I.IsPrime] (J : Ideal P) [hJ : J.IsPrime] (f : R →+* P) (hIJ : I = Ideal.comap f J) : IsLocalHom (Localization.localRingHom I J f hIJ)
• Localization.AtPrime.eq_maximalIdeal_iff_comap_eq 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
  {R : Type u_1} [CommSemiring R] {I : Ideal R} [hI : I.IsPrime] {J : Ideal (Localization.AtPrime I)} : Ideal.comap (algebraMap R (Localization.AtPrime I)) J = I ↔ J = IsLocalRing.maximalIdeal (Localization.AtPrime I)
• Localization.le_comap_primeCompl_iff 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
  {R : Type u_1} [CommSemiring R] {P : Type u_3} [CommSemiring P] {I : Ideal R} [hI : I.IsPrime] {J : Ideal P} [J.IsPrime] {f : R →+* P} : I.primeCompl ≤ Submonoid.comap f J.primeCompl ↔ Ideal.comap f J ≤ I
• Localization.AtPrime.instIsScalarTower 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
  {R : Type u_1} [CommSemiring R] {A : Type u_4} {B : Type u_5} [CommRing A] [CommRing B] [Algebra A B] [Algebra R A] [Algebra R B] [IsScalarTower R A B] (p : Ideal A) [p.IsPrime] (P : Ideal B) [P.IsPrime] [P.LiesOver p] : IsScalarTower R (Localization.AtPrime p) (Localization.AtPrime P)
• Localization.instNoZeroSMulDivisorsAtPrimeAlgebraMapSubmonoidPrimeComplOfNoZeroDivisorsOfIsDomain 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
  {R : Type u_4} {S : Type u_5} [CommRing R] [NoZeroDivisors R] {P : Ideal R} [CommRing S] [Algebra R S] [NoZeroSMulDivisors R S] [IsDomain S] [P.IsPrime] : NoZeroSMulDivisors (Localization.AtPrime P) (Localization (Algebra.algebraMapSubmonoid S P.primeCompl))
• IsLocalization.subsingleton_primeSpectrum_of_mem_minimalPrimes 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
  {R : Type u_5} [CommSemiring R] (p : Ideal R) (hp : p ∈ minimalPrimes R) (S : Type u_6) [CommSemiring S] [Algebra R S] [IsLocalization.AtPrime S p] : Subsingleton (PrimeSpectrum S)
• Localization.localRingHom_comp 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
  {R : Type u_1} [CommSemiring R] {P : Type u_3} [CommSemiring P] (I : Ideal R) [hI : I.IsPrime] {S : Type u_4} [CommSemiring S] (J : Ideal S) [hJ : J.IsPrime] (K : Ideal P) [hK : K.IsPrime] (f : R →+* S) (hIJ : I = Ideal.comap f J) (g : S →+* P) (hJK : J = Ideal.comap g K) : Localization.localRingHom I K (g.comp f) ⋯ = (Localization.localRingHom J K g hJK).comp (Localization.localRingHom I J f hIJ)
• Localization.AtPrime.instIsScalarTower_1 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
  {A : Type u_4} {B : Type u_5} {C : Type u_6} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra A C] [Algebra B C] [IsScalarTower A B C] (p : Ideal A) [p.IsPrime] (P : Ideal B) [P.IsPrime] [P.LiesOver p] (Q : Ideal C) [Q.IsPrime] [Q.LiesOver P] [Q.LiesOver p] : IsScalarTower (Localization.AtPrime p) (Localization.AtPrime P) (Localization.AtPrime Q)
• IsLocalization.AtPrime.coe_primeSpectrumOrderIso_apply_coe_asIdeal 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
  {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (I : Ideal R) [hI : I.IsPrime] [IsLocalization.AtPrime S I] (a✝ : PrimeSpectrum S) : ↑(↑((IsLocalization.AtPrime.primeSpectrumOrderIso S I) a✝)).asIdeal = ⇑(algebraMap R S) ⁻¹' ↑a✝.asIdeal
• Localization.localRingHom_to_map 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
  {R : Type u_1} [CommSemiring R] {P : Type u_3} [CommSemiring P] (I : Ideal R) [hI : I.IsPrime] (J : Ideal P) [J.IsPrime] (f : R →+* P) (hIJ : I = Ideal.comap f J) (x : R) : (Localization.localRingHom I J f hIJ) ((algebraMap R (Localization.AtPrime I)) x) = (algebraMap P (Localization.AtPrime J)) (f x)
• Localization.localRingHom_unique 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
  {R : Type u_1} [CommSemiring R] {P : Type u_3} [CommSemiring P] (I : Ideal R) [hI : I.IsPrime] (J : Ideal P) [J.IsPrime] (f : R →+* P) (hIJ : I = Ideal.comap f J) {j : Localization.AtPrime I →+* Localization.AtPrime J} (hj : ∀ (x : R), j ((algebraMap R (Localization.AtPrime I)) x) = (algebraMap P (Localization.AtPrime J)) (f x)) : Localization.localRingHom I J f hIJ = j
• Localization.AtPrime.mapPiEvalRingHom 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
  {ι : Type u_4} {R : ι → Type u_5} [(i : ι) → CommSemiring (R i)] {i : ι} (I : Ideal (R i)) [I.IsPrime] : Localization.AtPrime (Ideal.comap (Pi.evalRingHom R i) I) →+* Localization.AtPrime I
• Localization.localRingHom_mk' 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
  {R : Type u_1} [CommSemiring R] {P : Type u_3} [CommSemiring P] (I : Ideal R) [hI : I.IsPrime] (J : Ideal P) [J.IsPrime] (f : R →+* P) (hIJ : I = Ideal.comap f J) (x : R) (y : ↥I.primeCompl) : (Localization.localRingHom I J f hIJ) (IsLocalization.mk' (Localization.AtPrime I) x y) = IsLocalization.mk' (Localization.AtPrime J) (f x) ⟨f ↑y, ⋯⟩
• IsLocalization.AtPrime.coe_orderIsoOfPrime_apply_coe 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
  {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (I : Ideal R) [hI : I.IsPrime] [IsLocalization.AtPrime S I] (a✝ : { p // p.IsPrime }) : ↑↑((IsLocalization.AtPrime.orderIsoOfPrime S I) a✝) = ⇑(algebraMap R S) ⁻¹' ↑↑a✝
• Localization.AtPrime.mapPiEvalRingHom_comp_algebraMap 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
  {ι : Type u_4} {R : ι → Type u_5} [(i : ι) → CommSemiring (R i)] {i : ι} (I : Ideal (R i)) [I.IsPrime] : (Localization.AtPrime.mapPiEvalRingHom I).comp (algebraMap ((i : ι) → R i) (Localization.AtPrime (Ideal.comap (Pi.evalRingHom R i) I))) = (algebraMap (R i) (Localization.AtPrime I)).comp (Pi.evalRingHom R i)
• Localization.AtPrime.mapPiEvalRingHom_bijective 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
  {ι : Type u_4} {R : ι → Type u_5} [(i : ι) → CommSemiring (R i)] {i : ι} (I : Ideal (R i)) [I.IsPrime] : Function.Bijective ⇑(Localization.AtPrime.mapPiEvalRingHom I)
• IsLocalization.AtPrime.coe_primeSpectrumOrderIso_symm_apply_asIdeal 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
  {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (I : Ideal R) [hI : I.IsPrime] [IsLocalization.AtPrime S I] (a✝ : ↑(Set.Iic { asIdeal := I, isPrime := hI })) : ↑((RelIso.symm (IsLocalization.AtPrime.primeSpectrumOrderIso S I)) a✝).asIdeal = ⋂ s, ⋂ (_ : ↑↑((OrderIso.setCongr (fun p => p.IsPrime ∧ Disjoint ↑I.primeCompl ↑p) (fun p => p.IsPrime ∧ p ≤ I) ⋯).symm ⟨(↑a✝).asIdeal, ⋯⟩) ⊆ ⇑(algebraMap R S) ⁻¹' ↑s), ↑s
• Localization.AtPrime.mapPiEvalRingHom_algebraMap_apply 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
  {ι : Type u_4} {R : ι → Type u_5} [(i : ι) → CommSemiring (R i)] {i : ι} (I : Ideal (R i)) [I.IsPrime] {r : (i : ι) → R i} : (Localization.AtPrime.mapPiEvalRingHom I) ((algebraMap ((i : ι) → R i) (Localization.AtPrime (Ideal.comap (Pi.evalRingHom R i) I))) r) = (algebraMap (R i) (Localization.AtPrime I)) (r i)
• IsLocalization.AtPrime.coe_orderIsoOfPrime_symm_apply_coe 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
  {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (I : Ideal R) [hI : I.IsPrime] [IsLocalization.AtPrime S I] (a✝ : { p // p.IsPrime ∧ p ≤ I }) : ↑↑((RelIso.symm (IsLocalization.AtPrime.orderIsoOfPrime S I)) a✝) = ⋂ s, ⋂ (_ : ↑↑((OrderIso.setCongr (fun p => p.IsPrime ∧ Disjoint ↑I.primeCompl ↑p) (fun p => p.IsPrime ∧ p ≤ I) ⋯).symm a✝) ⊆ ⇑(algebraMap R S) ⁻¹' ↑s), ↑s
• LocalizedModule.AtPrime 📋 Mathlib.Algebra.Module.LocalizedModule.AtPrime
  {R : Type u_1} [CommSemiring R] (P : Ideal R) [P.IsPrime] (M : Type u_2) [AddCommMonoid M] [Module R M] : Type (max u_1 u_2)
• IsLocalizedModule.AtPrime 📋 Mathlib.Algebra.Module.LocalizedModule.AtPrime
  {R : Type u_1} {M : Type u_2} {M' : Type u_3} [CommSemiring R] (P : Ideal R) [P.IsPrime] [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') : Prop
• IsLocalizedModule.map_linearMap_of_isLocalization 📋 Mathlib.RingTheory.LocalProperties.Exactness
  {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] [Algebra R S] (Rₚ : Type u_5) (Sₚ : Type u_6) [CommSemiring Rₚ] [Algebra R Rₚ] [CommSemiring Sₚ] [Algebra S Sₚ] [Algebra R Sₚ] [IsScalarTower R S Sₚ] [Algebra Rₚ Sₚ] [IsScalarTower R Rₚ Sₚ] (p : Ideal R) [p.IsPrime] [IsLocalization.AtPrime Rₚ p] [IsLocalizedModule.AtPrime p ↑(IsScalarTower.toAlgHom R S Sₚ)] : (IsLocalizedModule.map p.primeCompl (Algebra.linearMap R Rₚ) ↑(IsScalarTower.toAlgHom R S Sₚ)) (Algebra.linearMap R S) = ↑R (Algebra.linearMap Rₚ Sₚ)
• instFlatAtPrime 📋 Mathlib.RingTheory.Flat.Localization
  {A : Type u_4} {B : Type u_5} [CommRing A] [CommRing B] [Algebra A B] [Module.Flat A B] (p : Ideal A) [p.IsPrime] (P : Ideal B) [P.IsPrime] [P.LiesOver p] : Module.Flat (Localization.AtPrime p) (Localization.AtPrime P)
• nilradical_eq_sInf 📋 Mathlib.RingTheory.Nilpotent.Lemmas
  (R : Type u_3) [CommSemiring R] : nilradical R = sInf {J | J.IsPrime}
• nilradical_le_prime 📋 Mathlib.RingTheory.Nilpotent.Lemmas
  {R : Type u_1} [CommSemiring R] (J : Ideal R) [H : J.IsPrime] : nilradical R ≤ J
• nilpotent_iff_mem_prime 📋 Mathlib.RingTheory.Nilpotent.Lemmas
  {R : Type u_1} [CommSemiring R] {x : R} : IsNilpotent x ↔ ∀ (J : Ideal R), J.IsPrime → x ∈ J
• Ideal.IsMaximal.of_liesOver_isMaximal 📋 Mathlib.RingTheory.Ideal.GoingUp
  {A : Type u_1} [CommRing A] {B : Type u_2} [CommRing B] [Algebra A B] [Algebra.IsIntegral A B] (P : Ideal B) (p : Ideal A) [P.LiesOver p] [hpm : p.IsMaximal] [P.IsPrime] : P.IsMaximal
• Ideal.nonempty_primesOver 📋 Mathlib.RingTheory.Ideal.GoingUp
  {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] [Nontrivial S] [Algebra.IsIntegral R S] [NoZeroSMulDivisors R S] (P : Ideal R) [P.IsPrime] : Nonempty ↑(P.primesOver S)
• Ideal.isMaximal_of_isIntegral_of_isMaximal_comap' 📋 Mathlib.RingTheory.Ideal.GoingUp
  {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] (f : R →+* S) (hf : f.IsIntegral) (I : Ideal S) [I.IsPrime] (hI : (Ideal.comap f I).IsMaximal) : I.IsMaximal
• Ideal.isMaximal_of_isIntegral_of_isMaximal_comap 📋 Mathlib.RingTheory.Ideal.GoingUp
  {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] [Algebra.IsIntegral R S] (I : Ideal S) [I.IsPrime] (hI : (Ideal.comap (algebraMap R S) I).IsMaximal) : I.IsMaximal
• Ideal.IsIntegralClosure.isMaximal_of_isMaximal_comap 📋 Mathlib.RingTheory.Ideal.GoingUp
  {R : Type u_1} [CommRing R] (S : Type u_2) [CommRing S] [Algebra R S] {A : Type u_3} [CommRing A] [Algebra R A] [Algebra A S] [IsScalarTower R A S] [IsIntegralClosure A R S] (I : Ideal A) [I.IsPrime] (hI : (Ideal.comap (algebraMap R A) I).IsMaximal) : I.IsMaximal
• Ideal.exists_ideal_over_prime_of_isIntegral_of_isDomain 📋 Mathlib.RingTheory.Ideal.GoingUp
  {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] [IsDomain S] [Algebra.IsIntegral R S] (P : Ideal R) [P.IsPrime] (hP : RingHom.ker (algebraMap R S) ≤ P) : ∃ Q, Q.IsPrime ∧ Ideal.comap (algebraMap R S) Q = P
• Ideal.exists_ideal_over_prime_of_isIntegral 📋 Mathlib.RingTheory.Ideal.GoingUp
  {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] [Algebra.IsIntegral R S] (P : Ideal R) [P.IsPrime] (I : Ideal S) (hIP : Ideal.comap (algebraMap R S) I ≤ P) : ∃ Q ≥ I, Q.IsPrime ∧ Ideal.comap (algebraMap R S) Q = P
• Ideal.exists_ideal_over_prime_of_isIntegral_of_isPrime 📋 Mathlib.RingTheory.Ideal.GoingUp
  {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] [Algebra.IsIntegral R S] (P : Ideal R) [P.IsPrime] (I : Ideal S) [I.IsPrime] (hIP : Ideal.comap (algebraMap R S) I ≤ P) : ∃ Q ≥ I, Q.IsPrime ∧ Ideal.comap (algebraMap R S) Q = P
• Ideal.IsIntegralClosure.comap_lt_comap 📋 Mathlib.RingTheory.Ideal.GoingUp
  {R : Type u_1} [CommRing R] (S : Type u_2) [CommRing S] [Algebra R S] {A : Type u_3} [CommRing A] [Algebra R A] [Algebra A S] [IsScalarTower R A S] [IsIntegralClosure A R S] {I J : Ideal A} [I.IsPrime] (I_lt_J : I < J) : Ideal.comap (algebraMap R A) I < Ideal.comap (algebraMap R A) J
• Ideal.comap_lt_comap_of_integral_mem_sdiff 📋 Mathlib.RingTheory.Ideal.GoingUp
  {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {I J : Ideal S} [Algebra R S] [hI : I.IsPrime] (hIJ : I ≤ J) {x : S} (mem : x ∈ ↑J \ ↑I) (integral : IsIntegral R x) : Ideal.comap (algebraMap R S) I < Ideal.comap (algebraMap R S) J
• Ideal.IntegralClosure.isMaximal_of_isMaximal_comap 📋 Mathlib.RingTheory.Ideal.GoingUp
  {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] (I : Ideal ↥(integralClosure R S)) [I.IsPrime] (hI : (Ideal.comap (algebraMap R ↥(integralClosure R S)) I).IsMaximal) : I.IsMaximal
• Ideal.IntegralClosure.comap_lt_comap 📋 Mathlib.RingTheory.Ideal.GoingUp
  {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] {I J : Ideal ↥(integralClosure R S)} [I.IsPrime] (I_lt_J : I < J) : Ideal.comap (algebraMap R ↥(integralClosure R S)) I < Ideal.comap (algebraMap R ↥(integralClosure R S)) J
• Ideal.comap_lt_comap_of_root_mem_sdiff 📋 Mathlib.RingTheory.Ideal.GoingUp
  {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {f : R →+* S} {I J : Ideal S} [I.IsPrime] (hIJ : I ≤ J) {r : S} (hr : r ∈ ↑J \ ↑I) {p : Polynomial R} (p_ne_zero : Polynomial.map (Ideal.Quotient.mk (Ideal.comap f I)) p ≠ 0) (hp : Polynomial.eval₂ f r p ∈ I) : Ideal.comap f I < Ideal.comap f J
• Ideal.exists_coeff_mem_comap_sdiff_comap_of_root_mem_sdiff 📋 Mathlib.RingTheory.Ideal.GoingUp
  {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {f : R →+* S} {I J : Ideal S} [I.IsPrime] (hIJ : I ≤ J) {r : S} (hr : r ∈ ↑J \ ↑I) {p : Polynomial R} (p_ne_zero : Polynomial.map (Ideal.Quotient.mk (Ideal.comap f I)) p ≠ 0) (hpI : Polynomial.eval₂ f r p ∈ I) : ∃ i, p.coeff i ∈ ↑(Ideal.comap f J) \ ↑(Ideal.comap f I)
• PrimeSpectrum.range_asIdeal 📋 Mathlib.RingTheory.Spectrum.Prime.Basic
  (R : Type u) [CommSemiring R] : Set.range PrimeSpectrum.asIdeal = {J | J.IsPrime}
• PrimeSpectrum.mk.congr_simp 📋 Mathlib.RingTheory.Spectrum.Prime.Basic
  {R : Type u_1} [CommSemiring R] (asIdeal asIdeal✝ : Ideal R) (e_asIdeal : asIdeal = asIdeal✝) (isPrime : asIdeal.IsPrime) : { asIdeal := asIdeal, isPrime := isPrime } = { asIdeal := asIdeal✝, isPrime := ⋯ }
• PrimeSpectrum.zeroLocus_eq_singleton 📋 Mathlib.RingTheory.Spectrum.Prime.Basic
  {R : Type u} [CommSemiring R] (m : Ideal R) [m.IsMaximal] : PrimeSpectrum.zeroLocus ↑m = {{ asIdeal := m, isPrime := ⋯ }}
• PrimeSpectrum.primeSpectrumProdOfSum.eq_1 📋 Mathlib.RingTheory.Spectrum.Prime.Basic
  (R : Type u) (S : Type v) [CommSemiring R] [CommSemiring S] (I : Ideal R) (isPrime : I.IsPrime) : PrimeSpectrum.primeSpectrumProdOfSum R S (Sum.inl { asIdeal := I, isPrime := isPrime }) = { asIdeal := I.prod ⊤, isPrime := ⋯ }
• PrimeSpectrum.primeSpectrumProdOfSum.eq_2 📋 Mathlib.RingTheory.Spectrum.Prime.Basic
  (R : Type u) (S : Type v) [CommSemiring R] [CommSemiring S] (J : Ideal S) (isPrime : J.IsPrime) : PrimeSpectrum.primeSpectrumProdOfSum R S (Sum.inr { asIdeal := J, isPrime := isPrime }) = { asIdeal := ⊤.prod J, isPrime := ⋯ }
• RingHom.SurjectiveOnStalks.exists_mul_eq_tmul 📋 Mathlib.RingTheory.SurjectiveOnStalks
  {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {T : Type u_3} [CommRing T] [Algebra R T] [Algebra R S] (hf₂ : (algebraMap R T).SurjectiveOnStalks) (x : TensorProduct R S T) (J : Ideal T) (hJ : J.IsPrime) : ∃ t r a, r • t ∉ J ∧ 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
• RingHom.SurjectiveOnStalks.eq_1 📋 Mathlib.RingTheory.SurjectiveOnStalks
  {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] (f : R →+* S) : f.SurjectiveOnStalks = ∀ (P : Ideal S) (x : P.IsPrime), Function.Surjective ⇑(Localization.localRingHom (Ideal.comap f P) P f ⋯)
• RingHom.surjective_localRingHom_iff 📋 Mathlib.RingTheory.SurjectiveOnStalks
  {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {f : R →+* S} (P : Ideal S) [P.IsPrime] : Function.Surjective ⇑(Localization.localRingHom (Ideal.comap f P) P f ⋯) ↔ ∀ (s : S), ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * s = c * f x
• Ideal.ResidueField 📋 Mathlib.RingTheory.LocalRing.ResidueField.Ideal
  {R : Type u_1} [CommRing R] (I : Ideal R) [I.IsPrime] : Type u_1
• instAlgebraQuotientIdealResidueField 📋 Mathlib.RingTheory.LocalRing.ResidueField.Ideal
  {R : Type u_1} [CommRing R] (I : Ideal R) [I.IsPrime] : Algebra (R ⧸ I) I.ResidueField
• instIsFractionRingQuotientIdealResidueField 📋 Mathlib.RingTheory.LocalRing.ResidueField.Ideal
  {R : Type u_1} [CommRing R] (I : Ideal R) [I.IsPrime] : IsFractionRing (R ⧸ I) I.ResidueField
• Ideal.surjectiveOnStalks_residueField 📋 Mathlib.RingTheory.LocalRing.ResidueField.Ideal
  {R : Type u_1} [CommRing R] (I : Ideal R) [I.IsPrime] : (algebraMap R I.ResidueField).SurjectiveOnStalks
• Ideal.ResidueField.map 📋 Mathlib.RingTheory.LocalRing.ResidueField.Ideal
  {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (I : Ideal R) [I.IsPrime] (J : Ideal S) [J.IsPrime] (f : R →+* S) (hf : I = Ideal.comap f J) : I.ResidueField →+* J.ResidueField
• Ideal.injective_algebraMap_quotient_residueField 📋 Mathlib.RingTheory.LocalRing.ResidueField.Ideal
  {R : Type u_1} [CommRing R] (I : Ideal R) [I.IsPrime] : Function.Injective ⇑(algebraMap (R ⧸ I) I.ResidueField)
• instIsScalarTowerQuotientIdealResidueField 📋 Mathlib.RingTheory.LocalRing.ResidueField.Ideal
  {R : Type u_1} [CommRing R] (I : Ideal R) [I.IsPrime] : IsScalarTower R (R ⧸ I) I.ResidueField

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 6ff4759 serving mathlib revision 519f454