Loogle!

Result

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

• Ideal 📋 Mathlib.RingTheory.Ideal.Defs
  (R : Type u) [Semiring R] : Type u
• Ideal.IsTwoSided 📋 Mathlib.RingTheory.Ideal.Defs
  {α : Type u} [Semiring α] (I : Ideal α) : Prop
• Ideal.instIsTwoSided 📋 Mathlib.RingTheory.Ideal.Defs
  {α : Type u} [CommSemiring α] (I : Ideal α) : I.IsTwoSided
• Module.eqIdeal 📋 Mathlib.RingTheory.Ideal.Defs
  (R : Type u_1) {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (m m' : M) : Ideal R
• Ideal.instIsTwoSided_1 📋 Mathlib.RingTheory.Ideal.Defs
  {α : Type u_1} [CommRing α] (I : Ideal α) : I.IsTwoSided
• Ideal.inertia 📋 Mathlib.RingTheory.Ideal.Defs
  {α : Type u} [Ring α] (G : Type u_1) [Group G] [MulAction G α] (I : Ideal α) : Subgroup G
• Ideal.zero_mem 📋 Mathlib.RingTheory.Ideal.Defs
  {α : Type u} [Semiring α] (I : Ideal α) : 0 ∈ I
• Ideal.ext 📋 Mathlib.RingTheory.Ideal.Defs
  {α : Type u} [Semiring α] {I J : Ideal α} (h : ∀ (x : α), x ∈ I ↔ x ∈ J) : I = J
• Ideal.ext_iff 📋 Mathlib.RingTheory.Ideal.Defs
  {α : Type u} [Semiring α] {I J : Ideal α} : I = J ↔ ∀ (x : α), x ∈ I ↔ x ∈ J
• Ideal.mul_mem_left 📋 Mathlib.RingTheory.Ideal.Defs
  {α : Type u} [Semiring α] (I : Ideal α) (a : α) {b : α} : b ∈ I → a * b ∈ I
• Ideal.mul_mem_right 📋 Mathlib.RingTheory.Ideal.Defs
  {α : Type u_1} {a : α} (b : α) [Semiring α] (I : Ideal α) [I.IsTwoSided] (h : a ∈ I) : a * b ∈ I
• Ideal.IsTwoSided.mk 📋 Mathlib.RingTheory.Ideal.Defs
  {α : Type u} [Semiring α] {I : Ideal α} (mul_mem_of_left : ∀ {a : α} (b : α), a ∈ I → a * b ∈ I) : I.IsTwoSided
• Ideal.IsTwoSided.mul_mem_of_left 📋 Mathlib.RingTheory.Ideal.Defs
  {α : Type u} {inst✝ : Semiring α} {I : Ideal α} [self : I.IsTwoSided] {a : α} (b : α) : a ∈ I → a * b ∈ I
• Ideal.isTwoSided_iff 📋 Mathlib.RingTheory.Ideal.Defs
  {α : Type u} [Semiring α] (I : Ideal α) : I.IsTwoSided ↔ ∀ {a : α} (b : α), a ∈ I → a * b ∈ I
• Ideal.unit_mul_mem_iff_mem 📋 Mathlib.RingTheory.Ideal.Defs
  {α : Type u} [Semiring α] (I : Ideal α) {x y : α} (hy : IsUnit y) : y * x ∈ I ↔ x ∈ I
• Ideal.pow_mem_of_mem 📋 Mathlib.RingTheory.Ideal.Defs
  {α : Type u} [Semiring α] (I : Ideal α) {a : α} (ha : a ∈ I) (n : ℕ) (hn : 0 < n) : a ^ n ∈ I
• Ideal.add_mem 📋 Mathlib.RingTheory.Ideal.Defs
  {α : Type u} [Semiring α] (I : Ideal α) {a b : α} : a ∈ I → b ∈ I → a + b ∈ I
• Ideal.pow_mem_of_pow_mem 📋 Mathlib.RingTheory.Ideal.Defs
  {α : Type u} [Semiring α] (I : Ideal α) {a : α} {m n : ℕ} (ha : a ^ m ∈ I) (h : m ≤ n) : a ^ n ∈ I
• Ideal.mem_of_dvd 📋 Mathlib.RingTheory.Ideal.Defs
  {α : Type u} {a b : α} [CommSemiring α] (I : Ideal α) (hab : a ∣ b) (ha : a ∈ I) : b ∈ I
• Ideal.neg_mem_iff 📋 Mathlib.RingTheory.Ideal.Defs
  {α : Type u} [Ring α] (I : Ideal α) {a : α} : -a ∈ I ↔ a ∈ I
• Ideal.mul_unit_mem_iff_mem 📋 Mathlib.RingTheory.Ideal.Defs
  {α : Type u} [CommSemiring α] (I : Ideal α) {x y : α} (hy : IsUnit y) : x * y ∈ I ↔ x ∈ I
• Ideal.mem_inertia 📋 Mathlib.RingTheory.Ideal.Defs
  {α : Type u} [Ring α] {G : Type u_1} [Group G] [MulAction G α] {I : Ideal α} {σ : G} : σ ∈ Ideal.inertia G I ↔ ∀ (x : α), σ • x - x ∈ I
• Ideal.add_mem_iff_left 📋 Mathlib.RingTheory.Ideal.Defs
  {α : Type u} [Ring α] (I : Ideal α) {a b : α} : b ∈ I → (a + b ∈ I ↔ a ∈ I)
• Ideal.add_mem_iff_right 📋 Mathlib.RingTheory.Ideal.Defs
  {α : Type u} [Ring α] (I : Ideal α) {a b : α} : a ∈ I → (a + b ∈ I ↔ b ∈ I)
• Ideal.sub_mem 📋 Mathlib.RingTheory.Ideal.Defs
  {α : Type u} [Ring α] (I : Ideal α) {a b : α} : a ∈ I → b ∈ I → a - b ∈ I
• Ideal.mul_sub_mul_mem 📋 Mathlib.RingTheory.Ideal.Defs
  {α : Type u} [Ring α] (I : Ideal α) {a b c d : α} [I.IsTwoSided] (h1 : a - b ∈ I) (h2 : c - d ∈ I) : a * c - b * d ∈ I
• Ideal.coe_mem_inertia 📋 Mathlib.RingTheory.Ideal.Defs
  {α : Type u} [Ring α] {G : Type u_1} [Group G] [MulAction G α] {I : Ideal α} {H : Subgroup G} {σ : ↥H} : ↑σ ∈ Ideal.inertia G I ↔ σ ∈ Ideal.inertia (↥H) I
• Ideal.instIsTwoSidedBot 📋 Mathlib.RingTheory.Ideal.Lattice
  {α : Type u} [Semiring α] : ⊥.IsTwoSided
• Ideal.instIsTwoSidedTop 📋 Mathlib.RingTheory.Ideal.Lattice
  {α : Type u} [Semiring α] : ⊤.IsTwoSided
• Ideal.instIsTwoSidedIInf 📋 Mathlib.RingTheory.Ideal.Lattice
  {α : Type u} [Semiring α] {ι : Sort u_1} (I : ι → Ideal α) [∀ (i : ι), (I i).IsTwoSided] : (⨅ i, I i).IsTwoSided
• Ideal.mem_bot 📋 Mathlib.RingTheory.Ideal.Lattice
  {R : Type u} [Semiring R] {x : R} : x ∈ ⊥ ↔ x = 0
• Ideal.eq_top_of_isUnit_mem 📋 Mathlib.RingTheory.Ideal.Lattice
  {α : Type u} [Semiring α] (I : Ideal α) {x : α} (hx : x ∈ I) (h : IsUnit x) : I = ⊤
• Ideal.eq_top_iff_one 📋 Mathlib.RingTheory.Ideal.Lattice
  {α : Type u} [Semiring α] (I : Ideal α) : I = ⊤ ↔ 1 ∈ I
• Ideal.ne_top_iff_one 📋 Mathlib.RingTheory.Ideal.Lattice
  {α : Type u} [Semiring α] (I : Ideal α) : I ≠ ⊤ ↔ 1 ∉ I
• Ideal.eq_bot_or_top 📋 Mathlib.RingTheory.Ideal.Lattice
  {K : Type u} [DivisionSemiring K] (I : Ideal K) : I = ⊥ ∨ I = ⊤
• Ideal.mem_iInf 📋 Mathlib.RingTheory.Ideal.Lattice
  {R : Type u} [Semiring R] {ι : Sort u_1} {I : ι → Ideal R} {x : R} : x ∈ iInf I ↔ ∀ (i : ι), x ∈ I i
• Ideal.eq_top_of_unit_mem 📋 Mathlib.RingTheory.Ideal.Lattice
  {α : Type u} [Semiring α] (I : Ideal α) (x y : α) (hx : x ∈ I) (h : y * x = 1) : I = ⊤
• Ideal.mem_sInf 📋 Mathlib.RingTheory.Ideal.Lattice
  {R : Type u} [Semiring R] {s : Set (Ideal R)} {x : R} : x ∈ sInf s ↔ ∀ ⦃I : Ideal R⦄, I ∈ s → x ∈ I
• Ideal.mem_sup_left 📋 Mathlib.RingTheory.Ideal.Lattice
  {R : Type u} [Semiring R] {S T : Ideal R} {x : R} : x ∈ S → x ∈ S ⊔ T
• Ideal.mem_sup_right 📋 Mathlib.RingTheory.Ideal.Lattice
  {R : Type u} [Semiring R] {S T : Ideal R} {x : R} : x ∈ T → x ∈ S ⊔ T
• Ideal.mem_iSup_of_mem 📋 Mathlib.RingTheory.Ideal.Lattice
  {R : Type u} [Semiring R] {ι : Sort u_1} {S : ι → Ideal R} (i : ι) {x : R} : x ∈ S i → x ∈ iSup S
• Ideal.mem_inf 📋 Mathlib.RingTheory.Ideal.Lattice
  {R : Type u} [Semiring R] {I J : Ideal R} {x : R} : x ∈ I ⊓ J ↔ x ∈ I ∧ x ∈ J
• Ideal.mem_sSup_of_mem 📋 Mathlib.RingTheory.Ideal.Lattice
  {R : Type u} [Semiring R] {S : Set (Ideal R)} {s : Ideal R} (hs : s ∈ S) {x : R} : x ∈ s → x ∈ sSup S
• 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 ≠ ⊤
• Ideal.isPrime_bot 📋 Mathlib.RingTheory.Ideal.Prime
  {α : Type u} [Semiring α] [Nontrivial α] [NoZeroDivisors α] : ⊥.IsPrime
• IsDomain.of_bot_isPrime 📋 Mathlib.RingTheory.Ideal.Prime
  (A : Type u_1) [Ring A] [hbp : ⊥.IsPrime] : IsDomain A
• Ideal.notMem_of_isUnit 📋 Mathlib.RingTheory.Ideal.Prime
  {α : Type u} [Semiring α] (I : Ideal α) [I.IsPrime] {x : α} (hx : IsUnit x) : x ∉ I
• 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.primeCompl_bot 📋 Mathlib.RingTheory.Ideal.Prime
  {α : Type u} [Semiring α] [Nontrivial α] [NoZeroDivisors α] : ⊥.primeCompl = nonZeroDivisors α
• 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.span 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [Semiring α] (s : Set α) : Ideal α
• Ideal.ofRel 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [Semiring α] (r : α → α → Prop) : Ideal α
• IsPrincipalIdealRing.mk 📋 Mathlib.RingTheory.Ideal.Span
  {R : Type u} [Semiring R] (principal : ∀ (S : Ideal R), Submodule.IsPrincipal S) : IsPrincipalIdealRing R
• IsPrincipalIdealRing.principal 📋 Mathlib.RingTheory.Ideal.Span
  {R : Type u} {inst✝ : Semiring R} [self : IsPrincipalIdealRing R] (S : Ideal R) : Submodule.IsPrincipal S
• isPrincipalIdealRing_iff 📋 Mathlib.RingTheory.Ideal.Span
  (R : Type u) [Semiring R] : IsPrincipalIdealRing R ↔ ∀ (S : Ideal R), Submodule.IsPrincipal S
• 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.isCompactElement_top 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [Semiring α] : IsCompactElement ⊤
• 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.zero_ne_one_of_proper 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [Semiring α] {I : Ideal α} (h : I ≠ ⊤) : 0 ≠ 1
• 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.mem_iff_of_associated 📋 Mathlib.RingTheory.Ideal.Span
  {α : Type u} [CommSemiring α] {I : Ideal α} {x y : α} (h : Associated x y) : x ∈ I ↔ y ∈ I
• 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
• Ideal.IsMaximal 📋 Mathlib.RingTheory.Ideal.Maximal
  {α : Type u} [Semiring α] (I : Ideal α) : Prop
• Ideal.instNontrivial 📋 Mathlib.RingTheory.Ideal.Maximal
  {α : Type u} [Semiring α] [Nontrivial α] : Nontrivial (Ideal α)
• Ideal.exists_maximal 📋 Mathlib.RingTheory.Ideal.Maximal
  (α : Type u) [Semiring α] [Nontrivial α] : ∃ M, M.IsMaximal
• 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.instIsCoatomic 📋 Mathlib.RingTheory.Ideal.Maximal
  {α : Type u} [Semiring α] : IsCoatomic (Ideal α)
• Ideal.IsMaximal.ne_top 📋 Mathlib.RingTheory.Ideal.Maximal
  {α : Type u} [Semiring α] {I : Ideal α} (h : I.IsMaximal) : I ≠ ⊤
• Ideal.bot_isMaximal 📋 Mathlib.RingTheory.Ideal.Maximal
  {K : Type u} [DivisionSemiring K] : ⊥.IsMaximal
• Ideal.IsMaximal.mk 📋 Mathlib.RingTheory.Ideal.Maximal
  {α : Type u} [Semiring α] {I : Ideal α} (out : IsCoatom I) : I.IsMaximal
• Ideal.IsMaximal.out 📋 Mathlib.RingTheory.Ideal.Maximal
  {α : Type u} {inst✝ : Semiring α} {I : Ideal α} [self : I.IsMaximal] : IsCoatom I
• Ideal.isMaximal_def 📋 Mathlib.RingTheory.Ideal.Maximal
  {α : Type u} [Semiring α] {I : Ideal α} : I.IsMaximal ↔ IsCoatom I
• Ideal.IsMaximal.lt_top 📋 Mathlib.RingTheory.Ideal.Maximal
  {α : Type u} [Semiring α] {I : Ideal α} (h : I.IsMaximal) : I < ⊤
• Ideal.exists_le_maximal 📋 Mathlib.RingTheory.Ideal.Maximal
  {α : Type u} [Semiring α] (I : Ideal α) (hI : I ≠ ⊤) : ∃ M, M.IsMaximal ∧ I ≤ M
• Ideal.ne_top_iff_exists_maximal 📋 Mathlib.RingTheory.Ideal.Maximal
  {α : Type u} [Semiring α] {I : Ideal α} : I ≠ ⊤ ↔ ∃ M, M.IsMaximal ∧ I ≤ M
• Ideal.IsMaximal.eq_of_le 📋 Mathlib.RingTheory.Ideal.Maximal
  {α : Type u} [Semiring α] {I J : Ideal α} (hI : I.IsMaximal) (hJ : J ≠ ⊤) (IJ : I ≤ J) : I = J
• Ideal.IsMaximal.eq_iff_le 📋 Mathlib.RingTheory.Ideal.Maximal
  {α : Type u} [Semiring α] {I J : Ideal α} (hI : I.IsMaximal) (hJ : J ≠ ⊤) : I = J ↔ I ≤ J
• 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.IsMaximal.coprime_of_ne 📋 Mathlib.RingTheory.Ideal.Maximal
  {α : Type u} [Semiring α] {M M' : Ideal α} (hM : M.IsMaximal) (hM' : M'.IsMaximal) (hne : M ≠ M') : M ⊔ M' = ⊤
• 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.maximal_of_no_maximal 📋 Mathlib.RingTheory.Ideal.Maximal
  {α : Type u} [Semiring α] {P : Ideal α} (hmax : ∀ (m : Ideal α), P < m → ¬m.IsMaximal) (J : Ideal α) (hPJ : P < J) : J = ⊤
• 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.IsMaximal.exists_inv 📋 Mathlib.RingTheory.Ideal.Maximal
  {α : Type u} [Semiring α] {I : Ideal α} (hI : I.IsMaximal) {x : α} (hx : x ∉ I) : ∃ y, ∃ i ∈ I, y * x + i = 1
• 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.isMaximal_iff 📋 Mathlib.RingTheory.Ideal.Maximal
  {α : Type u} [Semiring α] {I : Ideal α} : I.IsMaximal ↔ 1 ∉ I ∧ ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
• 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.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
• Ideal.instFinite 📋 Mathlib.RingTheory.Ideal.Basic
  {K : Type u_4} [DivisionSemiring K] : Finite (Ideal K)
• Ideal.equivFinTwo 📋 Mathlib.RingTheory.Ideal.Basic
  (K : Type u_4) [DivisionSemiring K] : Ideal K ≃ Fin 2
• Ideal.pi 📋 Mathlib.RingTheory.Ideal.Basic
  {ι : Type u_1} {R : ι → Type u_4} [(i : ι) → Semiring (R i)] (I : (i : ι) → Ideal (R i)) : Ideal ((i : ι) → R i)
• Ideal.instIsTwoSidedForallPi 📋 Mathlib.RingTheory.Ideal.Basic
  {ι : Type u_1} {R : ι → Type u_4} [(i : ι) → Semiring (R i)] (I : (i : ι) → Ideal (R i)) [∀ (i : ι), (I i).IsTwoSided] : (Ideal.pi I).IsTwoSided
• Ring.isField_iff_maximal_bot 📋 Mathlib.RingTheory.Ideal.Basic
  {R : Type u_4} [CommSemiring R] [Nontrivial R] : IsField R ↔ ⊥.IsMaximal
• Ring.ne_bot_of_isMaximal_of_not_isField 📋 Mathlib.RingTheory.Ideal.Basic
  {R : Type u_4} [CommSemiring R] [Nontrivial R] {M : Ideal R} (max : M.IsMaximal) (not_field : ¬IsField R) : M ≠ ⊥
• Ring.exists_maximal_of_not_isField 📋 Mathlib.RingTheory.Ideal.Basic
  {R : Type u_4} [CommSemiring R] [Nontrivial R] (h : ¬IsField R) : ∃ p, p ≠ ⊥ ∧ p.IsMaximal
• Ideal.isSimpleOrder 📋 Mathlib.RingTheory.Ideal.Basic
  {K : Type u_4} [DivisionSemiring K] : IsSimpleOrder (Ideal K)
• Ring.not_isField_iff_exists_prime 📋 Mathlib.RingTheory.Ideal.Basic
  {R : Type u_4} [CommSemiring R] [Nontrivial R] : ¬IsField R ↔ ∃ p, p ≠ ⊥ ∧ p.IsPrime
• 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}
• Ring.isField_iff_isSimpleOrder_ideal 📋 Mathlib.RingTheory.Ideal.Basic
  {R : Type u_4} [CommSemiring R] : IsField R ↔ IsSimpleOrder (Ideal R)
• Ring.not_isField_of_ne_of_ne 📋 Mathlib.RingTheory.Ideal.Basic
  {R : Type u_4} [CommSemiring R] [Nontrivial R] {I : Ideal R} (h_bot : I ≠ ⊥) (h_top : I ≠ ⊤) : ¬IsField R
• Ideal.bot_lt_of_maximal 📋 Mathlib.RingTheory.Ideal.Basic
  {R : Type u_4} [CommSemiring R] [Nontrivial R] (M : Ideal R) [hm : M.IsMaximal] (non_field : ¬IsField R) : ⊥ < M
• 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.prod_mem 📋 Mathlib.RingTheory.Ideal.Basic
  {α : Type u_2} [CommSemiring α] {ι : Type u_4} {f : ι → α} {s : Finset ι} (I : Ideal α) {i : ι} (hi : i ∈ s) (hfi : f i ∈ I) : ∏ i ∈ s, f i ∈ I
• 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.mem_pi 📋 Mathlib.RingTheory.Ideal.Basic
  {ι : Type u_1} {R : ι → Type u_4} [(i : ι) → Semiring (R i)] (I : (i : ι) → Ideal (R i)) (r : (i : ι) → R i) : r ∈ Ideal.pi I ↔ ∀ (i : ι), r i ∈ I i
• 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.single_mem_pi 📋 Mathlib.RingTheory.Ideal.Basic
  {ι : Type u_1} {R : ι → Type u_4} [(i : ι) → Semiring (R i)] {I : (i : ι) → Ideal (R i)} [DecidableEq ι] {i : ι} {r : R i} (hr : r ∈ I i) : Pi.single i r ∈ Ideal.pi I
• Ideal.pi_le_pi_iff 📋 Mathlib.RingTheory.Ideal.Basic
  {ι : Type u_1} {R : ι → Type u_4} [(i : ι) → Semiring (R i)] {I J : (i : ι) → Ideal (R i)} : Ideal.pi I ≤ Ideal.pi J ↔ I ≤ J
• 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)
• Ring.not_isField_iff_exists_ideal_bot_lt_and_lt_top 📋 Mathlib.RingTheory.Ideal.Basic
  {R : Type u_4} [CommSemiring R] [Nontrivial R] : ¬IsField R ↔ ∃ I, ⊥ < I ∧ I < ⊤
• Ideal.add_pow_add_pred_mem_of_pow_mem_of_commute 📋 Mathlib.RingTheory.Ideal.Basic
  {α : Type u_5} [Semiring α] (I : Ideal α) {a b : α} {m n : ℕ} (ha : a ^ m ∈ I) (hb : b ^ n ∈ I) (hab : Commute a b) : (a + b) ^ (m + n - 1) ∈ I
• Ideal.add_pow_mem_of_pow_mem_of_le_of_commute 📋 Mathlib.RingTheory.Ideal.Basic
  {α : Type u_5} [Semiring α] (I : Ideal α) {a b : α} {m n k : ℕ} (ha : a ^ m ∈ I) (hb : b ^ n ∈ I) (hk : m + n ≤ k + 1) (hab : Commute a b) : (a + b) ^ k ∈ I
• Ideal.add_pow_add_pred_mem_of_pow_mem 📋 Mathlib.RingTheory.Ideal.Basic
  {α : Type u_2} {a b : α} [CommSemiring α] (I : Ideal α) {m n : ℕ} (ha : a ^ m ∈ I) (hb : b ^ n ∈ I) : (a + b) ^ (m + n - 1) ∈ I
• Ideal.add_pow_mem_of_pow_mem_of_le 📋 Mathlib.RingTheory.Ideal.Basic
  {α : Type u_2} {a b : α} [CommSemiring α] (I : Ideal α) {m n k : ℕ} (ha : a ^ m ∈ I) (hb : b ^ n ∈ I) (hk : m + n ≤ k + 1) : (a + b) ^ k ∈ I
• Ideal.instHasQuotient 📋 Mathlib.RingTheory.Ideal.Quotient.Defs
  {R : Type u} [Ring R] : HasQuotient R (Ideal R)

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