Loogle!

Result

Found 118 declarations mentioning Ideal and DecidableEq. Of these, 17 match your pattern(s).

• Ideal.equivFinTwo 📋 Mathlib.RingTheory.Ideal.Basic
  (K : Type u_5) [DivisionSemiring K] [DecidableEq (Ideal K)] : Ideal K ≃ Fin 2
• count_le_of_ideal_ge 📋 Mathlib.RingTheory.DedekindDomain.Ideal
  {T : Type u_4} [CommRing T] [IsDedekindDomain T] [DecidableEq (Ideal T)] {I J : Ideal T} (h : I ≤ J) (hI : I ≠ ⊥) (K : Ideal T) : Multiset.count K (UniqueFactorizationMonoid.normalizedFactors J) ≤ Multiset.count K (UniqueFactorizationMonoid.normalizedFactors I)
• count_span_normalizedFactors_eq 📋 Mathlib.RingTheory.DedekindDomain.Ideal
  {R : Type u_1} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] [NormalizationMonoid R] [DecidableEq R] [DecidableEq (Ideal R)] {r X : R} (hr : r ≠ 0) (hX : Prime X) : Multiset.count (Ideal.span {X}) (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {r})) = Multiset.count (normalize X) (UniqueFactorizationMonoid.normalizedFactors r)
• count_span_normalizedFactors_eq_of_normUnit 📋 Mathlib.RingTheory.DedekindDomain.Ideal
  {R : Type u_1} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] [NormalizationMonoid R] [DecidableEq R] [DecidableEq (Ideal R)] {r X : R} (hr : r ≠ 0) (hX₁ : normUnit X = 1) (hX : Prime X) : Multiset.count (Ideal.span {X}) (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {r})) = Multiset.count X (UniqueFactorizationMonoid.normalizedFactors r)
• sup_eq_prod_inf_factors 📋 Mathlib.RingTheory.DedekindDomain.Ideal
  {T : Type u_4} [CommRing T] [IsDedekindDomain T] {I J : Ideal T} [DecidableEq (Ideal T)] (hI : I ≠ ⊥) (hJ : J ≠ ⊥) : I ⊔ J = (UniqueFactorizationMonoid.normalizedFactors I ∩ UniqueFactorizationMonoid.normalizedFactors J).prod
• irreducible_pow_sup 📋 Mathlib.RingTheory.DedekindDomain.Ideal
  {T : Type u_4} [CommRing T] [IsDedekindDomain T] {I J : Ideal T} [DecidableEq (Ideal T)] (hI : I ≠ ⊥) (hJ : Irreducible J) (n : ℕ) : J ^ n ⊔ I = J ^ min (Multiset.count J (UniqueFactorizationMonoid.normalizedFactors I)) n
• Ideal.count_normalizedFactors_eq 📋 Mathlib.RingTheory.DedekindDomain.Ideal
  {R : Type u_1} [CommRing R] [IsDedekindDomain R] {p x : Ideal R} [hp : p.IsPrime] {n : ℕ} (hle : x ≤ p ^ n) [DecidableEq (Ideal R)] (hlt : ¬x ≤ p ^ (n + 1)) : Multiset.count p (UniqueFactorizationMonoid.normalizedFactors x) = n
• Ideal.eq_prime_pow_mul_coprime 📋 Mathlib.RingTheory.DedekindDomain.Ideal
  {T : Type u_4} [CommRing T] [IsDedekindDomain T] [DecidableEq (Ideal T)] {I : Ideal T} (hI : I ≠ ⊥) (P : Ideal T) [hpm : P.IsMaximal] : ∃ Q, P ⊔ Q = ⊤ ∧ I = P ^ Multiset.count P (UniqueFactorizationMonoid.normalizedFactors I) * Q
• count_associates_factors_eq 📋 Mathlib.RingTheory.DedekindDomain.Ideal
  {R : Type u_1} [CommRing R] [IsDedekindDomain R] [DecidableEq (Ideal R)] [DecidableEq (Associates (Ideal R))] [(p : Associates (Ideal R)) → Decidable (Irreducible p)] {I J : Ideal R} (hI : I ≠ 0) (hJ : J.IsPrime) (hJ₀ : J ≠ ⊥) : (Associates.mk J).count (Associates.mk I).factors = Multiset.count J (UniqueFactorizationMonoid.normalizedFactors I)
• Submodule.isInternal_prime_power_torsion_of_is_torsion_by_ideal 📋 Mathlib.Algebra.Module.DedekindDomain
  {R : Type u} [CommRing R] [IsDomain R] {M : Type v} [AddCommGroup M] [Module R M] [IsDedekindDomain R] [DecidableEq (Ideal R)] {I : Ideal R} (hI : I ≠ ⊥) (hM : Module.IsTorsionBySet R M ↑I) : DirectSum.IsInternal fun p => Submodule.torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (UniqueFactorizationMonoid.factors I))
• Submodule.isInternal_prime_power_torsion 📋 Mathlib.Algebra.Module.DedekindDomain
  {R : Type u} [CommRing R] [IsDomain R] {M : Type v} [AddCommGroup M] [Module R M] [IsDedekindDomain R] [DecidableEq (Ideal R)] [Module.Finite R M] (hM : Module.IsTorsion R M) : DirectSum.IsInternal fun p => Submodule.torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (UniqueFactorizationMonoid.factors ⊤.annihilator))
• Submodule.isInternal_prime_power_torsion_of_pid 📋 Mathlib.Algebra.Module.PID
  {R : Type u} [CommRing R] [IsPrincipalIdealRing R] {M : Type v} [AddCommGroup M] [Module R M] [IsDomain R] [DecidableEq (Ideal R)] [Module.Finite R M] (hM : Module.IsTorsion R M) : DirectSum.IsInternal fun p => Submodule.torsionBy R M (Submodule.IsPrincipal.generator ↑p ^ Multiset.count (↑p) (UniqueFactorizationMonoid.factors ⊤.annihilator))
• Ideal.IsDedekindDomain.ramificationIdx_eq_factors_count 📋 Mathlib.NumberTheory.RamificationInertia.Basic
  {R : Type u} [CommRing R] {S : Type v} [CommRing S] {f : R →+* S} {p : Ideal R} {P : Ideal S} [IsDedekindDomain S] [DecidableEq (Ideal S)] (hp0 : Ideal.map f p ≠ ⊥) (hP : P.IsPrime) (hP0 : P ≠ ⊥) : Ideal.ramificationIdx f p P = Multiset.count P (UniqueFactorizationMonoid.factors (Ideal.map f p))
• Ideal.IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count 📋 Mathlib.NumberTheory.RamificationInertia.Basic
  {R : Type u} [CommRing R] {S : Type v} [CommRing S] {f : R →+* S} {p : Ideal R} {P : Ideal S} [IsDedekindDomain S] [DecidableEq (Ideal S)] (hp0 : Ideal.map f p ≠ ⊥) (hP : P.IsPrime) (hP0 : P ≠ ⊥) : Ideal.ramificationIdx f p P = Multiset.count P (UniqueFactorizationMonoid.normalizedFactors (Ideal.map f p))
• Ideal.IsLasker.minimal 📋 Mathlib.RingTheory.Lasker
  {R : Type u_1} [CommSemiring R] [DecidableEq (Ideal R)] (h : IsLasker R) (I : Ideal R) : ∃ t, t.inf id = I ∧ (∀ ⦃J : Ideal R⦄, J ∈ t → J.IsPrimary) ∧ (↑t).Pairwise (Function.onFun (fun x1 x2 => x1 ≠ x2) Ideal.radical) ∧ ∀ ⦃J : Ideal R⦄, J ∈ t → ¬(t.erase J).inf id ≤ J
• Ideal.decomposition_erase_inf 📋 Mathlib.RingTheory.Lasker
  {R : Type u_1} [CommSemiring R] [DecidableEq (Ideal R)] {I : Ideal R} {s : Finset (Ideal R)} (hs : s.inf id = I) : ∃ t ⊆ s, t.inf id = I ∧ ∀ ⦃J : Ideal R⦄, J ∈ t → ¬(t.erase J).inf id ≤ J
• Ideal.exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition 📋 Mathlib.RingTheory.Lasker
  {R : Type u_1} [CommSemiring R] [DecidableEq (Ideal R)] {I : Ideal R} {s : Finset (Ideal R)} (hs : s.inf id = I) (hs' : ∀ ⦃J : Ideal R⦄, J ∈ s → J.IsPrimary) : ∃ t, t.inf id = I ∧ (∀ ⦃J : Ideal R⦄, J ∈ t → J.IsPrimary) ∧ (↑t).Pairwise (Function.onFun (fun x1 x2 => x1 ≠ x2) Ideal.radical) ∧ ∀ ⦃J : Ideal R⦄, J ∈ t → ¬(t.erase J).inf id ≤ J

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 bce1d65