Loogle!

Result

Found 759 declarations mentioning Ideal.span. Of these, only the first 200 are shown.

• Ideal.span 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [Semiring α] (s : Set α) : Ideal α
• instIsPrincipalSpanSingletonSet 📋 Mathlib.RingTheory.Ideal.Span
  {R : Type u_1} [Semiring R] {x : R} : Submodule.IsPrincipal (Ideal.span {x})
• Ideal.span_univ 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [Semiring α] : Ideal.span Set.univ = ⊤
• Ideal.span_empty 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [Semiring α] : Ideal.span ∅ = ⊥
• Ideal.span_eq 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [Semiring α] (I : Ideal α) : Ideal.span ↑I = I
• Ideal.subset_span 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [Semiring α] {s : Set α} : s ⊆ ↑(Ideal.span s)
• Ideal.submodule_span_eq 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [Semiring α] {s : Set α} : Submodule.span α s = Ideal.span s
• Ideal.span_insert_zero 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [Semiring α] {s : Set α} : Ideal.span (insert 0 s) = Ideal.span s
• Ideal.mem_span_singleton_self 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [Semiring α] (x : α) : x ∈ Ideal.span {x}
• Ideal.mem_span_range_self 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [Semiring α] {β : Type u_1} {f : β → α} {x : β} : f x ∈ Ideal.span (Set.range f)
• Ideal.span_sdiff_singleton_zero 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [Semiring α] {s : Set α} : Ideal.span (s \ {0}) = Ideal.span s
• Ideal.span_zero 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [Semiring α] : Ideal.span 0 = ⊥
• Ideal.span_singleton_zero 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [Semiring α] : Ideal.span {0} = ⊥
• Ideal.span_one 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [Semiring α] : Ideal.span 1 = ⊤
• Ideal.span_pair_comm 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [Semiring α] {x y : α} : Ideal.span {x, y} = Ideal.span {y, x}
• Ideal.span_mono 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [Semiring α] {s t : Set α} : s ⊆ t → Ideal.span s ≤ Ideal.span t
• Ideal.span_pair_zero 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [Semiring α] (x : α) : Ideal.span {x, 0} = Ideal.span {x}
• Ideal.span_singleton_one 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [Semiring α] : Ideal.span {1} = ⊤
• Ideal.span_singleton_eq_bot 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [Semiring α] {x : α} : Ideal.span {x} = ⊥ ↔ x = 0
• Ideal.span_singleton_mul_left_unit 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [Semiring α] {a : α} (h2 : IsUnit a) (x : α) : Ideal.span {a * x} = Ideal.span {x}
• Ideal.span_singleton_abs 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [Ring α] (x : α) [LinearOrder α] : Ideal.span {|x|} = Ideal.span {x}
• Ideal.span_singleton_neg 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [Ring α] (x : α) : Ideal.span {-x} = Ideal.span {x}
• Ideal.span_eq_bot 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [Semiring α] {s : Set α} : Ideal.span s = ⊥ ↔ ∀ x ∈ s, x = 0
• Ideal.span_singleton_eq_span_singleton 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [CommSemiring α] [IsDomain α] {x y : α} : Ideal.span {x} = Ideal.span {y} ↔ Associated x y
• Ideal.span_insert_abs 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [Ring α] (x : α) (s : Set α) [LinearOrder α] : Ideal.span (insert |x| s) = Ideal.span (insert x s)
• Ideal.span_insert_neg 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [Ring α] (x : α) (s : Set α) : Ideal.span (insert (-x) s) = Ideal.span (insert x s)
• Ideal.span_singleton_eq_top 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [CommSemiring α] {x : α} : Ideal.span {x} = ⊤ ↔ IsUnit x
• Ideal.span_singleton_ne_top 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u_1} [CommSemiring α] {x : α} (hx : ¬IsUnit x) : Ideal.span {x} ≠ ⊤
• Ideal.mem_span_singleton' 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [Semiring α] {x y : α} : x ∈ Ideal.span {y} ↔ ∃ a, a * y = x
• Ideal.span_iUnion 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [Semiring α] {ι : Sort u_1} (s : ι → Set α) : Ideal.span (⋃ i, s i) = ⨆ i, Ideal.span (s i)
• Ideal.span_singleton_mul_right_unit 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [CommSemiring α] {a : α} (h2 : IsUnit a) (x : α) : Ideal.span {x * a} = Ideal.span {x}
• Ideal.span_le 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [Semiring α] {s : Set α} {I : Ideal α} : Ideal.span s ≤ I ↔ s ⊆ ↑I
• Ideal.span_pair_eq_span_left_iff_dvd 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [CommSemiring α] {x y : α} : Ideal.span {x, y} = Ideal.span {x} ↔ x ∣ y
• Ideal.span_pair_eq_span_right_iff_dvd 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [CommSemiring α] {x y : α} : Ideal.span {x, y} = Ideal.span {y} ↔ y ∣ x
• Ideal.span_union 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [Semiring α] (s t : Set α) : Ideal.span (s ∪ t) = Ideal.span s ⊔ Ideal.span t
• Ideal.span_range_eq_iSup 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [Semiring α] {ι : Type u_1} (x : ι → α) : Ideal.span (Set.range x) = ⨆ i, Ideal.span {x i}
• Ideal.span_pair_abs 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [Ring α] (x y : α) [LinearOrder α] : Ideal.span {x, |y|} = Ideal.span {x, y}
• Ideal.span_pair_add_left 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [Ring α] (x y : α) : Ideal.span {x, y + x} = Ideal.span {x, y}
• Ideal.span_pair_add_right 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [Ring α] (x y : α) : Ideal.span {x + y, y} = Ideal.span {x, y}
• Ideal.span_pair_left_add 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [Ring α] (x y : α) : Ideal.span {x, x + y} = Ideal.span {x, y}
• Ideal.span_pair_right_add 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [Ring α] (x y : α) : Ideal.span {y + x, y} = Ideal.span {x, y}
• Ideal.span_singleton_le_iff_mem 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [Semiring α] (I : Ideal α) {x : α} : Ideal.span {x} ≤ I ↔ x ∈ I
• Ideal.mem_span_singleton 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [CommSemiring α] {x y : α} : x ∈ Ideal.span {y} ↔ y ∣ x
• Ideal.span_pair_neg 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [Ring α] (x y : α) : Ideal.span {x, -y} = Ideal.span {x, y}
• Ideal.span_insert 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [Semiring α] (x : α) (s : Set α) : Ideal.span (insert x s) = Ideal.span {x} ⊔ Ideal.span s
• Ideal.span_pair_sub_left 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [Ring α] (x y : α) : Ideal.span {x, y - x} = Ideal.span {x, y}
• Ideal.span_pair_sub_left' 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [Ring α] (x y : α) : Ideal.span {y - x, y} = Ideal.span {x, y}
• Ideal.span_pair_sub_right 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [Ring α] (x y : α) : Ideal.span {x - y, y} = Ideal.span {x, y}
• Ideal.span_pair_sub_right' 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [Ring α] (x y : α) : Ideal.span {x, x - y} = Ideal.span {x, y}
• Ideal.span_range_eq_span_range_support 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [Semiring α] {ι : Type u_1} (x : ι → α) : Ideal.span (Set.range x) = Ideal.span (Set.range fun i => x ↑i)
• Ideal.iSup_eq_span 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [Semiring α] {ι : Sort u_1} (p : ι → Ideal α) : ⨆ i, p i = Ideal.span (⋃ i, ↑(p i))
• Ideal.span_eq_top_iff_finite 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [Semiring α] (s : Set α) : Ideal.span s = ⊤ ↔ ∃ s', ↑s' ⊆ s ∧ Ideal.span ↑s' = ⊤
• Ideal.mem_span 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [Semiring α] {s : Set α} (x : α) : x ∈ Ideal.span s ↔ ∀ (p : Ideal α), s ⊆ ↑p → x ∈ p
• Ideal.span_singleton_le_span_singleton 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [CommSemiring α] {x y : α} : Ideal.span {x} ≤ Ideal.span {y} ↔ y ∣ x
• Ideal.span_pair_add_left_mul 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [CommRing α] (x y z : α) : Ideal.span {x, y + x * z} = Ideal.span {x, y}
• Ideal.span_pair_add_mul_left 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [CommRing α] (x y z : α) : Ideal.span {x, y + z * x} = Ideal.span {x, y}
• Ideal.span_pair_add_mul_right 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [CommRing α] (x y z : α) : Ideal.span {x + z * y, y} = Ideal.span {x, y}
• Ideal.span_pair_add_right_mul 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [CommRing α] (x y z : α) : Ideal.span {x + y * z, y} = Ideal.span {x, y}
• Ideal.span_pair_left_mul_add 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [CommRing α] (x y z : α) : Ideal.span {x, x * z + y} = Ideal.span {x, y}
• Ideal.span_pair_mul_left_add 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [CommRing α] (x y z : α) : Ideal.span {x, z * x + y} = Ideal.span {x, y}
• Ideal.span_pair_mul_right_add 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [CommRing α] (x y z : α) : Ideal.span {z * y + x, y} = Ideal.span {x, y}
• Ideal.span_pair_right_mul_add 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [CommRing α] (x y z : α) : Ideal.span {y * z + x, y} = Ideal.span {x, y}
• Ideal.span_pair_sub_left_mul 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [CommRing α] (x y z : α) : Ideal.span {x, y - x * z} = Ideal.span {x, y}
• Ideal.span_pair_sub_mul_left 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [CommRing α] (x y z : α) : Ideal.span {x, y - z * x} = Ideal.span {x, y}
• Ideal.span_pair_sub_mul_right 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [CommRing α] (x y z : α) : Ideal.span {x - z * y, y} = Ideal.span {x, y}
• Ideal.span_pair_sub_right_mul 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [CommRing α] (x y z : α) : Ideal.span {x - y * z, y} = Ideal.span {x, y}
• Ideal.mem_span_pair 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [Semiring α] {x y z : α} : z ∈ Ideal.span {x, y} ↔ ∃ a b, a * x + b * y = z
• Ideal.mem_span_insert 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [Semiring α] {s : Set α} {x y : α} : x ∈ Ideal.span (insert y s) ↔ ∃ a, ∃ z ∈ Ideal.span s, x = a * y + z
• Ideal.factors_decreasing 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [CommSemiring α] [IsDomain α] (b₁ b₂ : α) (h₁ : b₁ ≠ 0) (h₂ : ¬IsUnit b₂) : Ideal.span {b₁ * b₂} < Ideal.span {b₁}
• Ideal.mem_span_insert' 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [Ring α] (x y : α) (s : Set α) : x ∈ Ideal.span (insert y s) ↔ ∃ a, x + a * y ∈ Ideal.span s
• Ideal.mem_span_singleton_sup 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [Semiring α] {x y : α} {I : Ideal α} : x ∈ Ideal.span {y} ⊔ I ↔ ∃ a, ∃ b ∈ I, a * y + b = x
• IsIdempotentElem.ker_toSpanSingleton_eq_span 📋 Mathlib.RingTheory.Ideal.Span
  {R : Type u_1} [CommRing R] {e : R} (he : IsIdempotentElem e) : (LinearMap.toSpanSingleton R R e).ker = Ideal.span {1 - e}
• IsIdempotentElem.ker_toSpanSingleton_one_sub_eq_span 📋 Mathlib.RingTheory.Ideal.Span
  {R : Type u_1} [CommRing R] {e : R} (he : IsIdempotentElem e) : (LinearMap.toSpanSingleton R R (1 - e)).ker = Ideal.span {e}
• Ideal.isPrime_span_singleton_of_prime 📋 Mathlib.RingTheory.Ideal.Maximal
  {α : Type u} [CommSemiring α] {p : α} (hp : Prime p) : (Ideal.span {p}).IsPrime
• Ideal.span_singleton_prime 📋 Mathlib.RingTheory.Ideal.Maximal
  {α : Type u} [CommSemiring α] {p : α} (hp : p ≠ 0) : (Ideal.span {p}).IsPrime ↔ Prime p
• Ideal.irreducible_of_isMaximal_span_singleton 📋 Mathlib.RingTheory.Ideal.Maximal
  {α : Type u} [CommSemiring α] [IsDomain α] {a : α} (ha : a ≠ 0) (max : (Ideal.span {a}).IsMaximal) : Irreducible a
• Ideal.irreducible_of_isMaximal_of_eq_span_singleton_of_not_isIdempotentElem 📋 Mathlib.RingTheory.Ideal.Maximal
  {α : Type u} [CommSemiring α] {a : α} (max : (Ideal.span {a}).IsMaximal) (idem : ∀ (x : α), Ideal.span {a} = Ideal.span {x} → ¬IsIdempotentElem x) : Irreducible a
• Ideal.span_singleton_lt_span_singleton 📋 Mathlib.RingTheory.Ideal.Maximal
  {α : Type u} [CommSemiring α] [IsDomain α] {x y : α} : Ideal.span {x} < Ideal.span {y} ↔ DvdNotUnit y x
• 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.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_disjoint_powers_of_span_eq_top 📋 Mathlib.RingTheory.Ideal.Maximal
  {α : Type u} [CommSemiring α] (s : Set α) (hs : Ideal.span s = ⊤) (I : Ideal α) (hI : I ≠ ⊤) : ∃ r ∈ s, Disjoint ↑I ↑(Submonoid.powers r)
• Ideal.pi_span 📋 Mathlib.RingTheory.Ideal.Basic
  {ι : Type u_1} {R : ι → Type u_4} [(i : ι) → Semiring (R i)] {r : (i : ι) → R i} : (Ideal.pi fun x => Ideal.span {r x}) = Ideal.span {r}
• Ideal.span_pow_eq_top 📋 Mathlib.RingTheory.Ideal.Basic
  {α : Type u_2} [CommSemiring α] (s : Set α) (hs : Ideal.span s = ⊤) (n : ℕ) : Ideal.span ((fun x => x ^ n) '' s) = ⊤
• Ideal.span_single_eq_top 📋 Mathlib.RingTheory.Ideal.Basic
  {ι : Type u_4} [DecidableEq ι] [Finite ι] (R : ι → Type u_5) [(i : ι) → Semiring (R i)] : Ideal.span (Set.range fun i => Pi.single i 1) = ⊤
• Ideal.span_range_pow_eq_top 📋 Mathlib.RingTheory.Ideal.Basic
  {α : Type u_2} [CommSemiring α] (s : Set α) (hs : Ideal.span s = ⊤) (n : ↑s → ℕ) : Ideal.span (Set.range fun x => ↑x ^ n x) = ⊤
• Ideal.pow_multiset_sum_mem_span_pow 📋 Mathlib.RingTheory.Ideal.Basic
  {α : Type u_2} [CommSemiring α] [DecidableEq α] (s : Multiset α) (n : ℕ) : s.sum ^ (s.card * n + 1) ∈ Ideal.span ↑(Multiset.map (fun x => x ^ (n + 1)) s).toFinset
• Ideal.sum_pow_mem_span_pow 📋 Mathlib.RingTheory.Ideal.Basic
  {α : Type u_2} [CommSemiring α] {ι : Type u_4} (s : Finset ι) (f : ι → α) (n : ℕ) : (∑ i ∈ s, f i) ^ (s.card * n + 1) ∈ Ideal.span ((fun i => f i ^ (n + 1)) '' ↑s)
• Ideal.Quotient.mk_span_range 📋 Mathlib.RingTheory.Ideal.Quotient.Basic
  {ι : Type u_1} {R : Type u_3} [Ring R] (f : ι → R) [(Ideal.span (Set.range f)).IsTwoSided] (i : ι) : (Ideal.Quotient.mk (Ideal.span (Set.range f))) (f i) = 0
• Ideal.Quotient.mk_singleton_self 📋 Mathlib.RingTheory.Ideal.Quotient.Basic
  {R : Type u_3} [Ring R] (x : R) [(Ideal.span {x}).IsTwoSided] : (Ideal.Quotient.mk (Ideal.span {x})) x = 0
• Ideal.Quotient.eq_zero_iff_dvd 📋 Mathlib.RingTheory.Ideal.Quotient.Basic
  {R : Type u_4} [CommRing R] (x y : R) : (Ideal.Quotient.mk (Ideal.span {x})) y = 0 ↔ x ∣ y
• Ideal.span_singleton_toAddSubgroup_eq_zmultiples 📋 Mathlib.RingTheory.Ideal.Operations
  (a : ℤ) : Submodule.toAddSubgroup (Ideal.span {a}) = AddSubgroup.zmultiples a
• Ideal.isCoprime_span_singleton_iff 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u} [CommSemiring R] (x y : R) : IsCoprime (Ideal.span {x}) (Ideal.span {y}) ↔ IsCoprime x y
• Ideal.prod_span 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u} [CommSemiring R] {ι : Type u_2} (s : Finset ι) (I : ι → Set R) : ∏ i ∈ s, Ideal.span (I i) = Ideal.span (∏ i ∈ s, I i)
• Ideal.mem_span_range_iff_exists_fun 📋 Mathlib.RingTheory.Ideal.Operations
  {α : Type u_1} {R : Type u_2} [Semiring R] [Fintype α] {x : R} {v : α → R} : x ∈ Ideal.span (Set.range v) ↔ ∃ c, ∑ i, c i * v i = x
• Ideal.multiset_prod_span_singleton 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u} [CommSemiring R] (m : Multiset R) : (Multiset.map (fun x => Ideal.span {x}) m).prod = Ideal.span {m.prod}
• Ideal.prod_span_singleton 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u} [CommSemiring R] {ι : Type u_2} (s : Finset ι) (I : ι → R) : ∏ i ∈ s, Ideal.span {I i} = Ideal.span {∏ i ∈ s, I i}
• Ideal.span_mul_span 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u} [Semiring R] (S T : Set R) [(Ideal.span S).IsTwoSided] : Ideal.span S * Ideal.span T = Ideal.span (S * T)
• Ideal.span_mul_span' 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u} [Semiring R] (S T : Set R) [(Ideal.span S).IsTwoSided] : Ideal.span S * Ideal.span T = Ideal.span (S * T)
• Finsupp.mem_ideal_span_range_iff_exists_finsupp 📋 Mathlib.RingTheory.Ideal.Operations
  {α : Type u_1} {R : Type u_2} [Semiring R] {x : R} {v : α → R} : x ∈ Ideal.span (Set.range v) ↔ ∃ c, (c.sum fun i a => a * v i) = x
• Ideal.iInf_span_singleton 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u} [CommSemiring R] {ι : Type u_2} [Fintype ι] {I : ι → R} (hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)) : ⨅ i, Ideal.span {I i} = Ideal.span {∏ i, I i}
• Ideal.span_singleton_pow 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u} [Semiring R] (s : R) [(Ideal.span {s}).IsTwoSided] (n : ℕ) : Ideal.span {s} ^ n = Ideal.span {s ^ n}
• Ideal.sup_eq_top_iff_isCoprime 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u_2} [CommSemiring R] (x y : R) : Ideal.span {x} ⊔ Ideal.span {y} = ⊤ ↔ IsCoprime x y
• Ideal.span_singleton_mul_span_singleton 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u} [Semiring R] (r s : R) [(Ideal.span {r}).IsTwoSided] : Ideal.span {r} * Ideal.span {s} = Ideal.span {r * s}
• Ideal.span_singleton_mul_left_injective 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u} [CommSemiring R] [IsDomain R] {x : R} (hx : x ≠ 0) : Function.Injective fun I => I * Ideal.span {x}
• Ideal.span_singleton_mul_right_injective 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u} [CommSemiring R] [IsDomain R] {x : R} (hx : x ≠ 0) : Function.Injective fun x_1 => Ideal.span {x} * x_1
• Submodule.set_smul_top_eq_span 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u_1} [CommSemiring R] (s : Set R) : s • ⊤ = Ideal.span s
• Submodule.smul_le_span 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u_1} [CommSemiring R] (s : Set R) (I : Ideal R) : s • I ≤ Ideal.span s
• Ideal.iInf_span_singleton_natCast 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u_2} [CommRing R] {ι : Type u_3} [Fintype ι] {I : ι → ℕ} (hI : Pairwise fun i j => (I i).Coprime (I j)) : ⨅ i, Ideal.span {↑(I i)} = Ideal.span {↑(∏ i, I i)}
• Ideal.mem_mul_span_singleton 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u} [Semiring R] {x y : R} {I : Ideal R} [I.IsTwoSided] : x ∈ I * Ideal.span {y} ↔ ∃ z ∈ I, z * y = x
• Ideal.finset_inf_span_singleton 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u} [CommSemiring R] {ι : Type u_2} (s : Finset ι) (I : ι → R) (hI : (↑s).Pairwise (Function.onFun IsCoprime I)) : (s.inf fun i => Ideal.span {I i}) = Ideal.span {∏ i ∈ s, I i}
• Ideal.span_singleton_mul_left_inj 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u} [Semiring R] {I J : Ideal R} [IsDomain R] [I.IsTwoSided] [J.IsTwoSided] {x : R} (hx : x ≠ 0) : I * Ideal.span {x} = J * Ideal.span {x} ↔ I = J
• Submodule.mem_of_span_top_of_smul_mem 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (M' : Submodule R M) (s : Set R) (hs : Ideal.span s = ⊤) (x : M) (H : ∀ (r : ↑s), ↑r • x ∈ M') : x ∈ M'
• Ideal.mem_span_singleton_mul 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u} [CommSemiring R] {x y : R} {I : Ideal R} : x ∈ Ideal.span {y} * I ↔ ∃ z ∈ I, y * z = x
• Submodule.span_smul_span 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (S : Set R) (T : Set M) [(Ideal.span S).IsTwoSided] : Ideal.span S • Submodule.span R T = Submodule.span R (S • T)
• Ideal.span_singleton_mul_right_inj 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u} [CommSemiring R] {I J : Ideal R} [IsDomain R] {x : R} (hx : x ≠ 0) : Ideal.span {x} * I = Ideal.span {x} * J ↔ I = J
• Submodule.coe_span_smul 📋 Mathlib.RingTheory.Ideal.Operations
  {R' : Type u_1} {M' : Type u_2} [CommSemiring R'] [AddCommMonoid M'] [Module R' M'] (s : Set R') (N : Submodule R' M') : ↑(Ideal.span s) • N = s • N
• Ideal.span_singleton_mul_left_mono 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u} [Semiring R] {I J : Ideal R} [IsDomain R] [I.IsTwoSided] [J.IsTwoSided] {x : R} (hx : x ≠ 0) : I * Ideal.span {x} ≤ J * Ideal.span {x} ↔ I ≤ J
• Submodule.span_smul_eq 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] (s : Set R) (N : Submodule R M) : Ideal.span s • N = s • N
• Ideal.span_pair_mul_span_pair 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u} [Semiring R] (w x y z : R) [(Ideal.span {w, x}).IsTwoSided] : Ideal.span {w, x} * Ideal.span {y, z} = Ideal.span {w * y, w * z, x * y, x * z}
• Ideal.span_singleton_mul_le_iff 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u} [CommSemiring R] {x : R} {I J : Ideal R} : Ideal.span {x} * I ≤ J ↔ ∀ z ∈ I, x * z ∈ J
• Associates.mk_ne_zero' 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u_1} [CommSemiring R] {r : R} : Associates.mk (Ideal.span {r}) ≠ 0 ↔ r ≠ 0
• Ideal.exists_subset_radical_span_sup_of_subset_radical_sup 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u_1} [CommSemiring R] (s : Set R) (I J : Ideal R) (hs : s ⊆ ↑(I ⊔ J).radical) : ∃ t, Set.range t ⊆ ↑I ∧ s ⊆ ↑(Ideal.span (Set.range t) ⊔ J).radical
• Ideal.le_span_singleton_mul_iff 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u} [CommSemiring R] {x : R} {I J : Ideal R} : I ≤ Ideal.span {x} * J ↔ ∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI
• Submodule.mem_of_span_eq_top_of_smul_pow_mem 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (M' : Submodule R M) (s : Set R) (hs : Ideal.span s = ⊤) (x : M) (H : ∀ (r : ↑s), ∃ n, ↑r ^ n • x ∈ M') : x ∈ M'
• Ideal.span_singleton_mul_right_mono 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u} [CommSemiring R] {I J : Ideal R} [IsDomain R] {x : R} (hx : x ≠ 0) : Ideal.span {x} * I ≤ Ideal.span {x} * J ↔ I ≤ J
• Ideal.span_singleton_nonZeroDivisors 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u_1} [CommSemiring R] [NoZeroDivisors R] {r : R} : Ideal.span {r} ∈ nonZeroDivisors (Ideal R) ↔ r ∈ nonZeroDivisors R
• Ideal.eq_span_singleton_mul 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u} [CommSemiring R] {x : R} (I J : Ideal R) : I = Ideal.span {x} * J ↔ (∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI) ∧ ∀ z ∈ J, x * z ∈ I
• Ideal.span_singleton_mul_le_span_singleton_mul 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u} [CommSemiring R] {x y : R} {I J : Ideal R} : Ideal.span {x} * I ≤ Ideal.span {y} * J ↔ ∀ zI ∈ I, ∃ zJ ∈ J, x * zI = y * zJ
• Submodule.ideal_span_singleton_smul 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (r : R) (N : Submodule R M) : Ideal.span {r} • N = r • N
• Ideal.span_singleton_mul_eq_span_singleton_mul 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u} [CommSemiring R] {x y : R} (I J : Ideal R) : Ideal.span {x} * I = Ideal.span {y} * J ↔ (∀ zI ∈ I, ∃ zJ ∈ J, x * zI = y * zJ) ∧ ∀ zJ ∈ J, ∃ zI ∈ I, x * zI = y * zJ
• Ideal.range_mul' 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u} [CommSemiring R] (a : R) : ((LinearMap.mul R R) a).range = Ideal.span {a}
• Ideal.range_mul 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u} [CommSemiring R] (A : Type u_2) [CommSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] (a : A) : ((LinearMap.mul R A) a).range = Submodule.restrictScalars R (Ideal.span {a})
• 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] (f : F) [RingHomClass F R S] (s : Set R) : Ideal.map f (Ideal.span s) = Ideal.span (⇑f '' s)
• RingHom.ker_evalRingHom 📋 Mathlib.RingTheory.Ideal.Maps
  {ι : Type u_1} [DecidableEq ι] (R : ι → Type u_2) [(i : ι) → CommRing (R i)] (i : ι) : RingHom.ker (Pi.evalRingHom R i) = Ideal.span {1 - Pi.single i 1}
• Ideal.span_prod 📋 Mathlib.RingTheory.Ideal.Prod
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {s : Set R} {t : Set S} (hst : s.Nonempty ↔ t.Nonempty) : Ideal.span (s ×ˢ t) = (Ideal.span s).prod (Ideal.span t)
• Ideal.span_prod_le 📋 Mathlib.RingTheory.Ideal.Prod
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {s : Set R} {t : Set S} : Ideal.span (s ×ˢ t) ≤ (Ideal.span s).prod (Ideal.span t)
• IsBezout.gcd 📋 Mathlib.RingTheory.PrincipalIdealDomain
  {R : Type u} [Ring R] (x y : R) [Submodule.IsPrincipal (Ideal.span {x, y})] : R
• Ideal.span_singleton_generator 📋 Mathlib.RingTheory.PrincipalIdealDomain
  {R : Type u} [Semiring R] (I : Ideal R) [Submodule.IsPrincipal I] : Ideal.span {Submodule.IsPrincipal.generator I} = I
• IsBezout.span_pair_isPrincipal 📋 Mathlib.RingTheory.PrincipalIdealDomain
  {R : Type u} [Ring R] [IsBezout R] (x y : R) : Submodule.IsPrincipal (Ideal.span {x, y})
• Submodule.IsPrincipal.associated_generator_span_self 📋 Mathlib.RingTheory.PrincipalIdealDomain
  {R : Type u} [CommSemiring R] [IsDomain R] (r : R) : Associated (Submodule.IsPrincipal.generator (Ideal.span {r})) r
• IsRelPrime.isCoprime 📋 Mathlib.RingTheory.PrincipalIdealDomain
  {R : Type u} [CommRing R] {x y : R} [Submodule.IsPrincipal (Ideal.span {x, y})] (h : IsRelPrime x y) : IsCoprime x y
• isRelPrime_iff_isCoprime 📋 Mathlib.RingTheory.PrincipalIdealDomain
  {R : Type u} [CommRing R] {x y : R} [Submodule.IsPrincipal (Ideal.span {x, y})] : IsRelPrime x y ↔ IsCoprime x y
• Ideal.exists_normalized_span_of_isPrincipal 📋 Mathlib.RingTheory.PrincipalIdealDomain
  {R : Type u_1} [CommSemiring R] [NormalizationMonoid R] (I : Ideal R) [Submodule.IsPrincipal I] : ∃ x, normalize x = x ∧ I = Ideal.span {x}
• IsBezout.gcd_dvd_left 📋 Mathlib.RingTheory.PrincipalIdealDomain
  {R : Type u} [CommRing R] (x y : R) [Submodule.IsPrincipal (Ideal.span {x, y})] : IsBezout.gcd x y ∣ x
• IsBezout.gcd_dvd_right 📋 Mathlib.RingTheory.PrincipalIdealDomain
  {R : Type u} [CommRing R] (x y : R) [Submodule.IsPrincipal (Ideal.span {x, y})] : IsBezout.gcd x y ∣ y
• span_gcd 📋 Mathlib.RingTheory.PrincipalIdealDomain
  {R : Type u} [CommRing R] [IsBezout R] [IsDomain R] [GCDMonoid R] (x y : R) : Ideal.span {gcd x y} = Ideal.span {x, y}
• IsBezout.associated_gcd_gcd 📋 Mathlib.RingTheory.PrincipalIdealDomain
  (R : Type u) [CommRing R] {x y : R} [Submodule.IsPrincipal (Ideal.span {x, y})] [GCDMonoid R] : Associated (IsBezout.gcd x y) (gcd x y)
• IsBezout.span_gcd 📋 Mathlib.RingTheory.PrincipalIdealDomain
  {R : Type u} [Ring R] (x y : R) [Submodule.IsPrincipal (Ideal.span {x, y})] : Ideal.span {IsBezout.gcd x y} = Ideal.span {x, y}
• IsBezout.span_gcd_eq_span_gcd 📋 Mathlib.RingTheory.PrincipalIdealDomain
  {R : Type u} [CommRing R] [IsBezout R] [IsDomain R] [GCDMonoid R] (x y : R) : Ideal.span {gcd x y} = Ideal.span {IsBezout.gcd x y}
• Submodule.IsPrincipal.dvd_generator_span_iff 📋 Mathlib.RingTheory.PrincipalIdealDomain
  {R : Type u} [CommSemiring R] {r : R} {s : Set R} [Submodule.IsPrincipal (Ideal.span s)] : r ∣ Submodule.IsPrincipal.generator (Ideal.span s) ↔ ∀ x ∈ s, r ∣ x
• IsBezout.dvd_gcd 📋 Mathlib.RingTheory.PrincipalIdealDomain
  {R : Type u} [CommRing R] {x y z : R} [Submodule.IsPrincipal (Ideal.span {x, y})] (hx : z ∣ x) (hy : z ∣ y) : z ∣ IsBezout.gcd x y
• IsBezout.gcd_eq_sum 📋 Mathlib.RingTheory.PrincipalIdealDomain
  {R : Type u} [CommRing R] (x y : R) [Submodule.IsPrincipal (Ideal.span {x, y})] : ∃ a b, a * x + b * y = IsBezout.gcd x y
• span_singleton_inf_span_singleton 📋 Mathlib.RingTheory.PrincipalIdealDomain
  {R : Type u} [EuclideanDomain R] [GCDMonoid R] (n m : R) : Ideal.span {n} ⊓ Ideal.span {m} = Ideal.span {lcm n m}
• dvd_generator_iff 📋 Mathlib.LinearAlgebra.FreeModule.PID
  {R : Type u_1} [CommSemiring R] {I : Ideal R} [Submodule.IsPrincipal I] {x : R} (hx : x ∈ I) : x ∣ Submodule.IsPrincipal.generator I ↔ I = Ideal.span {x}
• mem_span_C_coeff 📋 Mathlib.RingTheory.Polynomial.Basic
  {R : Type u} [Semiring R] {f : Polynomial R} : f ∈ Ideal.span {g | ∃ i, g = Polynomial.C (f.coeff i)}
• span_le_of_C_coeff_mem 📋 Mathlib.RingTheory.Polynomial.Basic
  {R : Type u} [Semiring R] {f : Polynomial R} {I : Ideal (Polynomial R)} (cf : ∀ (i : ℕ), Polynomial.C (f.coeff i) ∈ I) : Ideal.span {g | ∃ i, g = Polynomial.C (f.coeff i)} ≤ I
• EuclideanDomain.span_gcd 📋 Mathlib.RingTheory.EuclideanDomain
  {α : Type u_1} [EuclideanDomain α] [DecidableEq α] (x y : α) : Ideal.span {EuclideanDomain.gcd x y} = Ideal.span {x, y}
• IsLocalization.away_of_isIdempotentElem 📋 Mathlib.RingTheory.Localization.Away.Basic
  {R : Type u_4} {S : Type u_5} [CommRing R] [CommRing S] [Algebra R S] {e : R} (he : IsIdempotentElem e) (H : RingHom.ker (algebraMap R S) = Ideal.span {1 - e}) (H' : Function.Surjective ⇑(algebraMap R S)) : IsLocalization.Away e S
• Localization.algebraMap_injective_of_span_eq_top 📋 Mathlib.RingTheory.Localization.Away.Basic
  {R : Type u_1} [CommSemiring R] (s : Set R) (span_eq : Ideal.span s = ⊤) : Function.Injective ⇑(algebraMap R ((a : ↑s) → Localization.Away ↑a))
• Localization.existsUnique_algebraMap_eq_of_span_eq_top 📋 Mathlib.RingTheory.Localization.Away.Basic
  {R : Type u_1} [CommSemiring R] (s : Set R) (span_eq : Ideal.span s = ⊤) (f : (a : ↑s) → Localization.Away ↑a) (h : ∀ (a b : ↑s), (IsLocalization.Away.awayToAwayRight ↑a ↑b) (f a) = (IsLocalization.Away.awayToAwayLeft ↑b ↑a) (f b)) : ∃! r, ∀ (a : ↑s), (algebraMap R (Localization.Away ↑a)) r = f a
• CharacterModule.intSpanEquivQuotAddOrderOf 📋 Mathlib.Algebra.Module.CharacterModule
  {A : Type uA} [AddCommGroup A] (a : A) : ↥(ℤ ∙ a) ≃ₗ[ℤ] ℤ ⧸ Ideal.span {↑(addOrderOf a)}
• CharacterModule.intSpanEquivQuotAddOrderOf_apply_self 📋 Mathlib.Algebra.Module.CharacterModule
  {A : Type uA} [AddCommGroup A] (a : A) : (CharacterModule.intSpanEquivQuotAddOrderOf a) ⟨a, ⋯⟩ = Submodule.Quotient.mk 1
• CharacterModule.intSpanEquivQuotAddOrderOf_symm_apply_coe 📋 Mathlib.Algebra.Module.CharacterModule
  {A : Type uA} [AddCommGroup A] (a : A) (a✝ : ℤ ⧸ Ideal.span {↑(addOrderOf a)}) : ↑((CharacterModule.intSpanEquivQuotAddOrderOf a).symm a✝) = ↑((LinearMap.toSpanSingleton ℤ A a).quotKerEquivRange (((LinearMap.toSpanSingleton ℤ A a).ker.quotEquivOfEq (Ideal.span {↑(addOrderOf a)}) ⋯).symm a✝))
• CharacterModule.intSpanEquivQuotAddOrderOf_apply 📋 Mathlib.Algebra.Module.CharacterModule
  {A : Type uA} [AddCommGroup A] (a : A) (x : ↥(ℤ ∙ a)) : (CharacterModule.intSpanEquivQuotAddOrderOf a) x = ((LinearMap.toSpanSingleton ℤ A a).ker.quotEquivOfEq (Ideal.span {↑(addOrderOf a)}) ⋯) ((LinearMap.toSpanSingleton ℤ A a).quotKerEquivRange.symm ((LinearEquiv.ofEq (ℤ ∙ a) (LinearMap.toSpanSingleton ℤ A a).range ⋯) x))
• Ideal.smul_closure 📋 Mathlib.RingTheory.Ideal.Pointwise
  {M : Type u_1} {R : Type u_3} [Monoid M] [Semiring R] [MulSemiringAction M R] (a : M) (s : Set R) : a • Ideal.span s = Ideal.span (a • s)
• Ideal.colon_span 📋 Mathlib.RingTheory.Ideal.Colon
  {R : Type u_1} [CommSemiring R] {I : Ideal R} {S : Set R} : Submodule.colon I ↑(Ideal.span S) = Submodule.colon I S
• Ideal.mem_colon_span_singleton 📋 Mathlib.RingTheory.Ideal.Colon
  {R : Type u_1} [CommSemiring R] {I : Ideal R} {x r : R} : r ∈ Submodule.colon I ↑(Ideal.span {x}) ↔ r * 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.under R (Ideal.map (algebraMap R (Localization.Away f)) I)
• IsLocalization.ideal_eq_iInf_under_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.under R (Ideal.map (algebraMap R (Localization.Away f)) I)
• isRadical_iff_span_singleton 📋 Mathlib.RingTheory.Nilpotent.Lemmas
  {R : Type u_1} {y : R} [CommSemiring R] : IsRadical y ↔ (Ideal.span {y}).IsRadical
• Module.eq_zero_of_isLocalized_span 📋 Mathlib.RingTheory.LocalProperties.Submodule
  {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (s : Set R) (span_eq : Ideal.span s = ⊤) (Mₚ : ↑s → Type u_5) [(r : ↑s) → AddCommMonoid (Mₚ r)] [(r : ↑s) → Module R (Mₚ r)] (f : (r : ↑s) → M →ₗ[R] Mₚ r) [∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)] (x : M) (h : ∀ (r : ↑s), (f r) x = 0) : x = 0
• Submodule.eq_bot_of_isLocalized₀_span 📋 Mathlib.RingTheory.LocalProperties.Submodule
  {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (s : Set R) (span_eq : Ideal.span s = ⊤) (Mₚ : ↑s → Type u_5) [(r : ↑s) → AddCommMonoid (Mₚ r)] [(r : ↑s) → Module R (Mₚ r)] (f : (r : ↑s) → M →ₗ[R] Mₚ r) [∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)] {N : Submodule R M} (h : ∀ (r : ↑s), Submodule.localized₀ (Submonoid.powers ↑r) (f r) N = ⊥) : N = ⊥
• Submodule.eq_top_of_isLocalized₀_span 📋 Mathlib.RingTheory.LocalProperties.Submodule
  {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (s : Set R) (span_eq : Ideal.span s = ⊤) (Mₚ : ↑s → Type u_5) [(r : ↑s) → AddCommMonoid (Mₚ r)] [(r : ↑s) → Module R (Mₚ r)] (f : (r : ↑s) → M →ₗ[R] Mₚ r) [∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)] {N : Submodule R M} (h : ∀ (r : ↑s), Submodule.localized₀ (Submonoid.powers ↑r) (f r) N = ⊤) : N = ⊤
• Submodule.eq_of_isLocalized₀_span 📋 Mathlib.RingTheory.LocalProperties.Submodule
  {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (s : Set R) (span_eq : Ideal.span s = ⊤) (Mₚ : ↑s → Type u_5) [(r : ↑s) → AddCommMonoid (Mₚ r)] [(r : ↑s) → Module R (Mₚ r)] (f : (r : ↑s) → M →ₗ[R] Mₚ r) [∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)] {N P : Submodule R M} (h : ∀ (r : ↑s), Submodule.localized₀ (Submonoid.powers ↑r) (f r) N = Submodule.localized₀ (Submonoid.powers ↑r) (f r) P) : N = P
• Module.eq_of_isLocalized_span 📋 Mathlib.RingTheory.LocalProperties.Submodule
  {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (s : Set R) (span_eq : Ideal.span s = ⊤) (Mₚ : ↑s → Type u_5) [(r : ↑s) → AddCommMonoid (Mₚ r)] [(r : ↑s) → Module R (Mₚ r)] (f : (r : ↑s) → M →ₗ[R] Mₚ r) [∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)] (x y : M) (h : ∀ (r : ↑s), (f r) x = (f r) y) : x = y
• Submodule.le_of_isLocalized_span 📋 Mathlib.RingTheory.LocalProperties.Submodule
  {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (s : Set R) (span_eq : Ideal.span s = ⊤) (Mₚ : ↑s → Type u_5) [(r : ↑s) → AddCommMonoid (Mₚ r)] [(r : ↑s) → Module R (Mₚ r)] (f : (r : ↑s) → M →ₗ[R] Mₚ r) [∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)] {N P : Submodule R M} (h : ∀ (r : ↑s), Submodule.localized₀ (Submonoid.powers ↑r) (f r) N ≤ Submodule.localized₀ (Submonoid.powers ↑r) (f r) P) : N ≤ P
• Submodule.mem_of_isLocalized_span 📋 Mathlib.RingTheory.LocalProperties.Submodule
  {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (s : Set R) (span_eq : Ideal.span s = ⊤) (Mₚ : ↑s → Type u_5) [(r : ↑s) → AddCommMonoid (Mₚ r)] [(r : ↑s) → Module R (Mₚ r)] (f : (r : ↑s) → M →ₗ[R] Mₚ r) [∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)] {m : M} {N : Submodule R M} (h : ∀ (r : ↑s), (f r) m ∈ Submodule.localized₀ (Submonoid.powers ↑r) (f r) N) : m ∈ N
• Submodule.eq_bot_of_isLocalized'_span 📋 Mathlib.RingTheory.LocalProperties.Submodule
  {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (s : Set R) (span_eq : Ideal.span s = ⊤) (Rₚ : ↑s → Type u_4) [(r : ↑s) → CommSemiring (Rₚ r)] [(r : ↑s) → Algebra R (Rₚ r)] [∀ (r : ↑s), IsLocalization.Away (↑r) (Rₚ r)] (Mₚ : ↑s → Type u_5) [(r : ↑s) → AddCommMonoid (Mₚ r)] [(r : ↑s) → Module R (Mₚ r)] [(r : ↑s) → Module (Rₚ r) (Mₚ r)] [∀ (r : ↑s), IsScalarTower R (Rₚ r) (Mₚ r)] (f : (r : ↑s) → M →ₗ[R] Mₚ r) [∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)] {N : Submodule R M} (h : ∀ (r : ↑s), Submodule.localized' (Rₚ r) (Submonoid.powers ↑r) (f r) N = ⊥) : N = ⊥
• Submodule.eq_top_of_isLocalized'_span 📋 Mathlib.RingTheory.LocalProperties.Submodule
  {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (s : Set R) (span_eq : Ideal.span s = ⊤) (Rₚ : ↑s → Type u_4) [(r : ↑s) → CommSemiring (Rₚ r)] [(r : ↑s) → Algebra R (Rₚ r)] [∀ (r : ↑s), IsLocalization.Away (↑r) (Rₚ r)] (Mₚ : ↑s → Type u_5) [(r : ↑s) → AddCommMonoid (Mₚ r)] [(r : ↑s) → Module R (Mₚ r)] [(r : ↑s) → Module (Rₚ r) (Mₚ r)] [∀ (r : ↑s), IsScalarTower R (Rₚ r) (Mₚ r)] (f : (r : ↑s) → M →ₗ[R] Mₚ r) [∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)] {N : Submodule R M} (h : ∀ (r : ↑s), Submodule.localized' (Rₚ r) (Submonoid.powers ↑r) (f r) N = ⊤) : N = ⊤
• Submodule.eq_of_isLocalized'_span 📋 Mathlib.RingTheory.LocalProperties.Submodule
  {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (s : Set R) (span_eq : Ideal.span s = ⊤) (Rₚ : ↑s → Type u_4) [(r : ↑s) → CommSemiring (Rₚ r)] [(r : ↑s) → Algebra R (Rₚ r)] [∀ (r : ↑s), IsLocalization.Away (↑r) (Rₚ r)] (Mₚ : ↑s → Type u_5) [(r : ↑s) → AddCommMonoid (Mₚ r)] [(r : ↑s) → Module R (Mₚ r)] [(r : ↑s) → Module (Rₚ r) (Mₚ r)] [∀ (r : ↑s), IsScalarTower R (Rₚ r) (Mₚ r)] (f : (r : ↑s) → M →ₗ[R] Mₚ r) [∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)] {N P : Submodule R M} (h : ∀ (r : ↑s), Submodule.localized' (Rₚ r) (Submonoid.powers ↑r) (f r) N = Submodule.localized' (Rₚ r) (Submonoid.powers ↑r) (f r) P) : N = P
• bijective_of_isLocalization_of_span_eq_top 📋 Mathlib.RingTheory.LocalProperties.Exactness
  {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] {s : Set R} (hs : Ideal.span s = ⊤) (Rᵣ : ↑s → Type u_3) [(r : ↑s) → CommSemiring (Rᵣ r)] [(r : ↑s) → Algebra R (Rᵣ r)] (Sᵣ : ↑s → Type u_4) [(r : ↑s) → CommSemiring (Sᵣ r)] [(r : ↑s) → Algebra S (Sᵣ r)] (f : R →+* S) [∀ (r : ↑s), IsLocalization.Away (↑r) (Rᵣ r)] [∀ (r : ↑s), IsLocalization.Away (f ↑r) (Sᵣ r)] (h : ∀ (r : ↑s), Function.Bijective ⇑(IsLocalization.Away.map (Rᵣ r) (Sᵣ r) f ↑r)) : Function.Bijective ⇑f
• injective_of_isLocalization_of_span_eq_top 📋 Mathlib.RingTheory.LocalProperties.Exactness
  {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] {s : Set R} (hs : Ideal.span s = ⊤) (Rᵣ : ↑s → Type u_3) [(r : ↑s) → CommSemiring (Rᵣ r)] [(r : ↑s) → Algebra R (Rᵣ r)] (Sᵣ : ↑s → Type u_4) [(r : ↑s) → CommSemiring (Sᵣ r)] [(r : ↑s) → Algebra S (Sᵣ r)] (f : R →+* S) [∀ (r : ↑s), IsLocalization.Away (↑r) (Rᵣ r)] [∀ (r : ↑s), IsLocalization.Away (f ↑r) (Sᵣ r)] (h : ∀ (r : ↑s), Function.Injective ⇑(IsLocalization.Away.map (Rᵣ r) (Sᵣ r) f ↑r)) : Function.Injective ⇑f
• surjective_of_isLocalization_of_span_eq_top 📋 Mathlib.RingTheory.LocalProperties.Exactness
  {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] {s : Set R} (hs : Ideal.span s = ⊤) (Rᵣ : ↑s → Type u_3) [(r : ↑s) → CommSemiring (Rᵣ r)] [(r : ↑s) → Algebra R (Rᵣ r)] (Sᵣ : ↑s → Type u_4) [(r : ↑s) → CommSemiring (Sᵣ r)] [(r : ↑s) → Algebra S (Sᵣ r)] (f : R →+* S) [∀ (r : ↑s), IsLocalization.Away (↑r) (Rᵣ r)] [∀ (r : ↑s), IsLocalization.Away (f ↑r) (Sᵣ r)] (h : ∀ (r : ↑s), Function.Surjective ⇑(IsLocalization.Away.map (Rᵣ r) (Sᵣ r) f ↑r)) : Function.Surjective ⇑f
• bijective_of_isLocalized_span 📋 Mathlib.RingTheory.LocalProperties.Exactness
  {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (s : Set R) (spn : Ideal.span s = ⊤) (Mₚ : ↑s → Type u_5) [(r : ↑s) → AddCommMonoid (Mₚ r)] [(r : ↑s) → Module R (Mₚ r)] (f : (r : ↑s) → M →ₗ[R] Mₚ r) [∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)] (Nₚ : ↑s → Type u_6) [(r : ↑s) → AddCommMonoid (Nₚ r)] [(r : ↑s) → Module R (Nₚ r)] (g : (r : ↑s) → N →ₗ[R] Nₚ r) [∀ (r : ↑s), IsLocalizedModule.Away (↑r) (g r)] (F : M →ₗ[R] N) (H : ∀ (r : ↑s), Function.Bijective ⇑((IsLocalizedModule.map (Submonoid.powers ↑r) (f r) (g r)) F)) : Function.Bijective ⇑F
• injective_of_isLocalized_span 📋 Mathlib.RingTheory.LocalProperties.Exactness
  {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (s : Set R) (spn : Ideal.span s = ⊤) (Mₚ : ↑s → Type u_5) [(r : ↑s) → AddCommMonoid (Mₚ r)] [(r : ↑s) → Module R (Mₚ r)] (f : (r : ↑s) → M →ₗ[R] Mₚ r) [∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)] (Nₚ : ↑s → Type u_6) [(r : ↑s) → AddCommMonoid (Nₚ r)] [(r : ↑s) → Module R (Nₚ r)] (g : (r : ↑s) → N →ₗ[R] Nₚ r) [∀ (r : ↑s), IsLocalizedModule.Away (↑r) (g r)] (F : M →ₗ[R] N) (H : ∀ (r : ↑s), Function.Injective ⇑((IsLocalizedModule.map (Submonoid.powers ↑r) (f r) (g r)) F)) : Function.Injective ⇑F
• surjective_of_isLocalized_span 📋 Mathlib.RingTheory.LocalProperties.Exactness
  {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (s : Set R) (spn : Ideal.span s = ⊤) (Mₚ : ↑s → Type u_5) [(r : ↑s) → AddCommMonoid (Mₚ r)] [(r : ↑s) → Module R (Mₚ r)] (f : (r : ↑s) → M →ₗ[R] Mₚ r) [∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)] (Nₚ : ↑s → Type u_6) [(r : ↑s) → AddCommMonoid (Nₚ r)] [(r : ↑s) → Module R (Nₚ r)] (g : (r : ↑s) → N →ₗ[R] Nₚ r) [∀ (r : ↑s), IsLocalizedModule.Away (↑r) (g r)] (F : M →ₗ[R] N) (H : ∀ (r : ↑s), Function.Surjective ⇑((IsLocalizedModule.map (Submonoid.powers ↑r) (f r) (g r)) F)) : Function.Surjective ⇑F
• exact_of_isLocalized_span 📋 Mathlib.RingTheory.LocalProperties.Exactness
  {R : Type u_1} {M : Type u_2} {N : Type u_3} {L : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid L] [Module R L] (s : Set R) (spn : Ideal.span s = ⊤) (Mₚ : ↑s → Type u_5) [(r : ↑s) → AddCommMonoid (Mₚ r)] [(r : ↑s) → Module R (Mₚ r)] (f : (r : ↑s) → M →ₗ[R] Mₚ r) [∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)] (Nₚ : ↑s → Type u_6) [(r : ↑s) → AddCommMonoid (Nₚ r)] [(r : ↑s) → Module R (Nₚ r)] (g : (r : ↑s) → N →ₗ[R] Nₚ r) [∀ (r : ↑s), IsLocalizedModule.Away (↑r) (g r)] (Lₚ : ↑s → Type u_7) [(r : ↑s) → AddCommMonoid (Lₚ r)] [(r : ↑s) → Module R (Lₚ r)] (h : (r : ↑s) → L →ₗ[R] Lₚ r) [∀ (r : ↑s), IsLocalizedModule.Away (↑r) (h r)] (F : M →ₗ[R] N) (G : N →ₗ[R] L) (H : ∀ (r : ↑s), Function.Exact ⇑((IsLocalizedModule.map (Submonoid.powers ↑r) (f r) (g r)) F) ⇑((IsLocalizedModule.map (Submonoid.powers ↑r) (g r) (h r)) G)) : Function.Exact ⇑F ⇑G
• bijective_of_localized_span 📋 Mathlib.RingTheory.LocalProperties.Exactness
  {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (s : Set R) (spn : Ideal.span s = ⊤) (f : M →ₗ[R] N) (h : ∀ (r : ↑s), Function.Bijective ⇑((LocalizedModule.map (Submonoid.powers ↑r)) f)) : Function.Bijective ⇑f
• injective_of_localized_span 📋 Mathlib.RingTheory.LocalProperties.Exactness
  {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (s : Set R) (spn : Ideal.span s = ⊤) (f : M →ₗ[R] N) (h : ∀ (r : ↑s), Function.Injective ⇑((LocalizedModule.map (Submonoid.powers ↑r)) f)) : Function.Injective ⇑f
• surjective_of_localized_span 📋 Mathlib.RingTheory.LocalProperties.Exactness
  {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (s : Set R) (spn : Ideal.span s = ⊤) (f : M →ₗ[R] N) (h : ∀ (r : ↑s), Function.Surjective ⇑((LocalizedModule.map (Submonoid.powers ↑r)) f)) : Function.Surjective ⇑f
• exact_of_localized_span 📋 Mathlib.RingTheory.LocalProperties.Exactness
  {R : Type u_1} {M : Type u_2} {N : Type u_3} {L : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid L] [Module R L] (s : Set R) (spn : Ideal.span s = ⊤) (f : M →ₗ[R] N) (g : N →ₗ[R] L) (h : ∀ (r : ↑s), Function.Exact ⇑((LocalizedModule.map (Submonoid.powers ↑r)) f) ⇑((LocalizedModule.map (Submonoid.powers ↑r)) g)) : Function.Exact ⇑f ⇑g
• Module.flat_of_localized_span 📋 Mathlib.RingTheory.Flat.Localization
  (S : Type u_2) [CommSemiring S] (M : Type u_3) [AddCommMonoid M] [Module S M] (s : Set S) (spn : Ideal.span s = ⊤) (h : ∀ (r : ↑s), Module.Flat S (LocalizedModule.Away (↑r) M)) : Module.Flat S M
• Module.flat_of_isLocalized_span 📋 Mathlib.RingTheory.Flat.Localization
  {R : Type u_1} (S : Type u_2) [CommSemiring R] [CommSemiring S] [Algebra R S] (M : Type u_3) [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower R S M] (s : Set S) (spn : Ideal.span s = ⊤) (Mₛ : ↑s → Type u_5) [(r : ↑s) → AddCommMonoid (Mₛ r)] [(r : ↑s) → Module R (Mₛ r)] [(r : ↑s) → Module S (Mₛ r)] [∀ (r : ↑s), IsScalarTower R S (Mₛ r)] (g : (r : ↑s) → M →ₗ[S] Mₛ r) [∀ (r : ↑s), IsLocalizedModule.Away (↑r) (g r)] (H : ∀ (r : ↑s), Module.Flat R (Mₛ r)) : Module.Flat R M
• Algebra.tensorQuotientTensorEquiv 📋 Mathlib.RingTheory.TensorProduct.Quotient
  {R : Type u_1} {R' : Type u_2} (R'' : Type u_3) {S : Type u_4} [CommRing R] [CommRing R'] [CommRing R''] [CommRing S] [Algebra R R'] [Algebra R R''] [Algebra R' R''] [IsScalarTower R R' R''] [Algebra R S] (e : TensorProduct R R' S) : TensorProduct R' R'' (TensorProduct R R' S ⧸ Ideal.span {e}) ≃ₐ[R''] TensorProduct R R'' S ⧸ Ideal.span {(Algebra.TensorProduct.rTensor S (Algebra.ofId R' R'')) e}
• Algebra.tensorQuotientTensorEquiv_tmul 📋 Mathlib.RingTheory.TensorProduct.Quotient
  {R : Type u_1} {R' : Type u_2} {R'' : Type u_3} {S : Type u_4} [CommRing R] [CommRing R'] [CommRing R''] [CommRing S] [Algebra R R'] [Algebra R R''] [Algebra R' R''] [IsScalarTower R R' R''] [Algebra R S] (e : TensorProduct R R' S) (a : R'') (b : R') (c : S) : (Algebra.tensorQuotientTensorEquiv R'' e) (a ⊗ₜ[R'] (Ideal.Quotient.mk (Ideal.span {e})) (b ⊗ₜ[R] c)) = (Ideal.Quotient.mk (Ideal.span {(Algebra.TensorProduct.rTensor S (Algebra.ofId R' R'')) e})) ((a * (algebraMap R' R'') b) ⊗ₜ[R] c)
• Algebra.tensorQuotientTensorEquiv_symm_tmul 📋 Mathlib.RingTheory.TensorProduct.Quotient
  {R : Type u_1} {R' : Type u_2} {R'' : Type u_3} {S : Type u_4} [CommRing R] [CommRing R'] [CommRing R''] [CommRing S] [Algebra R R'] [Algebra R R''] [Algebra R' R''] [IsScalarTower R R' R''] [Algebra R S] (e : TensorProduct R R' S) (a : R'') (b : S) : (Algebra.tensorQuotientTensorEquiv R'' e).symm ((Ideal.Quotient.mk (Ideal.span {(Algebra.TensorProduct.rTensor S (Algebra.ofId R' R'')) e})) (a ⊗ₜ[R] b)) = a ⊗ₜ[R'] (Ideal.Quotient.mk (Ideal.span {e})) (1 ⊗ₜ[R] b)
• IsLocalization.coeSubmodule_span 📋 Mathlib.RingTheory.Localization.Submodule
  {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (s : Set R) : IsLocalization.coeSubmodule S (Ideal.span s) = Submodule.span R (⇑(algebraMap R S) '' s)
• IsLocalization.coeSubmodule_span_singleton 📋 Mathlib.RingTheory.Localization.Submodule
  {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (x : R) : IsLocalization.coeSubmodule S (Ideal.span {x}) = R ∙ (algebraMap R S) x
• IsLocalization.mem_span_map 📋 Mathlib.RingTheory.Localization.Submodule
  {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] {x : S} {a : Set R} : x ∈ Ideal.span (⇑(algebraMap R S) '' a) ↔ ∃ y ∈ Ideal.span a, ∃ z, x = IsLocalization.mk' S y z
• RingHom.OfLocalizationSpanTarget.ofIsLocalization 📋 Mathlib.RingTheory.LocalProperties.Basic
  {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : RingHom.OfLocalizationSpanTarget fun {R S} [CommRing R] [CommRing S] => P) (hP' : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P) {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) (s : Set S) (hs : Ideal.span s = ⊤) (hT : ∀ (r : ↑s), ∃ T x x_1, ∃ (_ : IsLocalization.Away (↑r) T), P ((algebraMap S T).comp f)) : P f

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. 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.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

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. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision 69fae59