Loogle!

Result

Found 752 declarations mentioning Subring. Of these, only the first 200 are shown.

• Subring 📋 Mathlib.Algebra.Ring.Subring.Defs
  (R : Type u) [NonAssocRing R] : Type u
• Subring.instPartialOrder 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] : PartialOrder (Subring R)
• Subring.instSetLike 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] : SetLike (Subring R) R
• Subring.toNonUnitalSubring 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (S : Subring R) : NonUnitalSubring R
• Subring.toSubsemiring 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (self : Subring R) : Subsemiring R
• Subring.instSubringClass 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] : SubringClass (Subring R) R
• Subring.toAddSubgroup 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (self : Subring R) : AddSubgroup R
• Subring.toSubsemiring_injective 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] : Function.Injective Subring.toSubsemiring
• Subring.ofClass 📋 Mathlib.Algebra.Ring.Subring.Defs
  {S : Type u_1} {R : Type u_2} [NonAssocRing R] [SetLike S R] [SubringClass S R] (s : S) : Subring R
• Subring.toAddSubgroup_injective 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] : Function.Injective Subring.toAddSubgroup
• Subring.toNonUnitalSubring_toSubring 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (S : Subring R) : S.toNonUnitalSubring.toSubring ⋯ = S
• Subring.copy 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (S : Subring R) (s : Set R) (hs : s = ↑S) : Subring R
• Subring.instNontrivialSubtypeMem 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u_1} [NonAssocRing R] [Nontrivial R] (s : Subring R) : Nontrivial ↥s
• Subring.toSubmonoid_injective 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] : Function.Injective fun s => s.toSubmonoid
• Subring.toSubsemiring_inj 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] {s t : Subring R} : s.toSubsemiring = t.toSubsemiring ↔ s = t
• Subring.copy_eq 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (S : Subring R) (s : Set R) (hs : s = ↑S) : S.copy s hs = S
• Subring.toRing 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u_1} [Ring R] (s : Subring R) : Ring ↥s
• Subring.coe_toSubsemiring 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (s : Subring R) : ↑s.toSubsemiring = ↑s
• Subring.one_mem 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (s : Subring R) : 1 ∈ s
• Subring.zero_mem 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (s : Subring R) : 0 ∈ s
• Subring.coe_ofClass 📋 Mathlib.Algebra.Ring.Subring.Defs
  {S : Type u_1} {R : Type u_2} [NonAssocRing R] [SetLike S R] [SubringClass S R] (s : S) : ↑(Subring.ofClass s) = ↑s
• Subring.coe_copy 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (S : Subring R) (s : Set R) (hs : s = ↑S) : ↑(S.copy s hs) = s
• Subring.toCommRing 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u_1} [CommRing R] (s : Subring R) : CommRing ↥s
• Subring.coe_toAddSubgroup 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (s : Subring R) : ↑s.toAddSubgroup = ↑s
• Subring.one_mem_toNonUnitalSubring 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (S : Subring R) : 1 ∈ S.toNonUnitalSubring
• NonUnitalSubring.toSubring 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (S : NonUnitalSubring R) (h1 : 1 ∈ S) : Subring R
• Subring.coe_toSubmonoid 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (s : Subring R) : ↑s.toSubmonoid = ↑s
• Subring.ext 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] {S T : Subring R} (h : ∀ (x : R), x ∈ S ↔ x ∈ T) : S = T
• Subring.mem_toSubsemiring 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] {s : Subring R} {x : R} : x ∈ s.toSubsemiring ↔ x ∈ s
• Subring.ext_iff 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] {S T : Subring R} : S = T ↔ ∀ (x : R), x ∈ S ↔ x ∈ T
• Subring.neg_mem 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (s : Subring R) {x : R} : x ∈ s → -x ∈ s
• Subring.mem_toAddSubgroup 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] {s : Subring R} {x : R} : x ∈ s.toAddSubgroup ↔ x ∈ s
• Subring.zsmul_mem 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (s : Subring R) {x : R} (hx : x ∈ s) (n : ℤ) : n • x ∈ s
• Subring.mem_carrier 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] {s : Subring R} {x : R} : x ∈ s.carrier ↔ x ∈ s
• Subring.subtype 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (s : Subring R) : ↥s →+* R
• Subsemiring.toSubring 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (s : Subsemiring R) (hneg : -1 ∈ s) : Subring R
• Subring.mem_toSubmonoid 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] {s : Subring R} {x : R} : x ∈ s.toSubmonoid ↔ x ∈ s
• Subring.instIsDomainSubtypeMem 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u_1} [Ring R] [IsDomain R] (s : Subring R) : IsDomain ↥s
• Subring.add_mem 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (s : Subring R) {x y : R} : x ∈ s → y ∈ s → x + y ∈ s
• Subring.mul_mem 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (s : Subring R) {x y : R} : x ∈ s → y ∈ s → x * y ∈ s
• Subring.pow_mem 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u_1} [Ring R] (s : Subring R) {x : R} (hx : x ∈ s) (n : ℕ) : x ^ n ∈ s
• Subring.sub_mem 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (s : Subring R) {x y : R} (hx : x ∈ s) (hy : y ∈ s) : x - y ∈ s
• Subring.mk' 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (s : Set R) (sm : Submonoid R) (sa : AddSubgroup R) (hm : ↑sm = s) (ha : ↑sa = s) : Subring R
• Subring.copy_toSubsemiring 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (S : Subring R) (s : Set R) (hs : s = ↑S) : (S.copy s hs).toSubsemiring = { carrier := s, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯ }
• Subring.coe_mk' 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (s : Set R) (sm : Submonoid R) (sa : AddSubgroup R) (hm : ↑sm = s) (ha : ↑sa = s) : ↑(Subring.mk' s sm sa hm ha) = s
• Subring.mk 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (toSubsemiring : Subsemiring R) (neg_mem' : ∀ {x : R}, x ∈ toSubsemiring.carrier → -x ∈ toSubsemiring.carrier) : Subring R
• Subring.neg_mem' 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (self : Subring R) {x : R} : x ∈ self.carrier → -x ∈ self.carrier
• Subring.mem_mk' 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] {s : Set R} {sm : Submonoid R} (hm : ↑sm = s) {sa : AddSubgroup R} (ha : ↑sa = s) {x : R} : x ∈ Subring.mk' s sm sa hm ha ↔ x ∈ s
• Subring.coe_set_mk 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (S : Subsemiring R) (h : ∀ {x : R}, x ∈ S.carrier → -x ∈ S.carrier) : ↑{ toSubsemiring := S, neg_mem' := h } = ↑S
• Subring.coe_intCast 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (s : Subring R) (n : ℤ) : ↑↑n = ↑n
• Subring.coe_one 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (s : Subring R) : ↑1 = 1
• Subring.coe_neg 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (s : Subring R) (x : ↥s) : ↑(-x) = -↑x
• Subring.mem_mk 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] {S : Subsemiring R} {x : R} (h : ∀ {x : R}, x ∈ S.carrier → -x ∈ S.carrier) : x ∈ { toSubsemiring := S, neg_mem' := h } ↔ x ∈ S
• Subring.coe_zero 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (s : Subring R) : ↑0 = 0
• Subring.coe_natCast 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (s : Subring R) (n : ℕ) : ↑↑n = ↑n
• Subring.subtype_injective 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (s : Subring R) : Function.Injective ⇑s.subtype
• Subring.instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMulForallForallNeg 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] : CanLift (Set R) (Subring R) SetLike.coe fun s => 0 ∈ s ∧ (∀ {x y : R}, x ∈ s → y ∈ s → x + y ∈ s) ∧ 1 ∈ s ∧ (∀ {x y : R}, x ∈ s → y ∈ s → x * y ∈ s) ∧ ∀ {x : R}, x ∈ s → -x ∈ s
• Subring.mk_eq_zero 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (s : Subring R) {x : R} (hx : x ∈ s) : ⟨x, hx⟩ = 0 ↔ x = 0
• Subring.coe_eq_zero_iff 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (s : Subring R) {x : ↥s} : ↑x = 0 ↔ x = 0
• Subring.coe_subtype 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (s : Subring R) : ⇑s.subtype = Subtype.val
• Subring.subtype_apply 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] {s : Subring R} (x : ↥s) : s.subtype x = ↑x
• Subring.instNoZeroDivisorsSubtypeMem 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u_1} [NonAssocRing R] [NoZeroDivisors R] (s : Subring R) : NoZeroDivisors ↥s
• Subring.coe_pow 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u_1} [Ring R] (s : Subring R) (x : ↥s) (n : ℕ) : ↑(x ^ n) = ↑x ^ n
• Subring.mk_le_mk 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] {S S' : Subsemiring R} (h₁ : ∀ {x : R}, x ∈ S.carrier → -x ∈ S.carrier) (h₂ : ∀ {x : R}, x ∈ S'.carrier → -x ∈ S'.carrier) : { toSubsemiring := S, neg_mem' := h₁ } ≤ { toSubsemiring := S', neg_mem' := h₂ } ↔ S ≤ S'
• Subring.coe_add 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (s : Subring R) (x y : ↥s) : ↑(x + y) = ↑x + ↑y
• Subring.coe_mul 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (s : Subring R) (x y : ↥s) : ↑(x * y) = ↑x * ↑y
• Subring.center 📋 Mathlib.Algebra.Ring.Subring.Basic
  (R : Type u) [NonAssocRing R] : Subring R
• Subring.instBot 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] : Bot (Subring R)
• Subring.instCompleteLattice 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] : CompleteLattice (Subring R)
• Subring.instInfSet 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] : InfSet (Subring R)
• Subring.instInhabited 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] : Inhabited (Subring R)
• Subring.instMin 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] : Min (Subring R)
• Subring.instTop 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] : Top (Subring R)
• Subring.closure 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] (s : Set R) : Subring R
• Subring.centralizer 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u_1} [Ring R] (s : Set R) : Subring R
• RingHom.range 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] (f : R →+* S) : Subring S
• Subring.centralizer_univ 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u_1} [Ring R] : Subring.centralizer Set.univ = Subring.center R
• Subring.closure_univ 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] : Subring.closure Set.univ = ⊤
• Subring.comap 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] (f : R →+* S) (s : Subring S) : Subring R
• Subring.map 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] (f : R →+* S) (s : Subring R) : Subring S
• Subring.prod 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] (s : Subring R) (t : Subring S) : Subring (R × S)
• Subring.closure_empty 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] : Subring.closure ∅ = ⊥
• Subring.map_id 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] (s : Subring R) : Subring.map (RingHom.id R) s = s
• Subring.closure_eq 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] (s : Subring R) : Subring.closure ↑s = s
• Subring.coe_top 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] : ↑⊤ = Set.univ
• Subring.subset_closure 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] {s : Set R} : s ⊆ ↑(Subring.closure s)
• Subring.mem_top 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] (x : R) : x ∈ ⊤
• RingHom.eqLocus 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] {S : Type v} [Semiring S] (f g : R →+* S) : Subring R
• Subring.coe_center 📋 Mathlib.Algebra.Ring.Subring.Basic
  (R : Type u) [NonAssocRing R] : ↑(Subring.center R) = Set.center R
• Subring.instFintypeSubtypeMemTop 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u_1} [NonAssocRing R] [Fintype R] : Fintype ↥⊤
• Subring.toSubsemiring_top 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] : ⊤.toSubsemiring = ⊤
• Subring.instCommRingSubtypeMemCenter 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u_1} [Ring R] : CommRing ↥(Subring.center R)
• Subring.mem_closure_of_mem 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] {s : Set R} {x : R} (hx : x ∈ s) : x ∈ Subring.closure s
• RingHom.eqLocus_same 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] {S : Type v} [Semiring S] (f : R →+* S) : f.eqLocus f = ⊤
• Subring.center_eq_top 📋 Mathlib.Algebra.Ring.Subring.Basic
  (R : Type u_1) [CommRing R] : Subring.center R = ⊤
• Subring.coe_bot 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] : ↑⊥ = Set.range Int.cast
• Subring.toSubsemiring_mono 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] : Monotone Subring.toSubsemiring
• Subring.toSubsemiring_strictMono 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] : StrictMono Subring.toSubsemiring
• Subring.closure_insert_intCast 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] (n : ℤ) (s : Set R) : Subring.closure (insert (↑n) s) = Subring.closure s
• Subring.closure_singleton_intCast 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] (n : ℤ) : Subring.closure {↑n} = ⊥
• Subring.coe_centralizer 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u_1} [Ring R] (s : Set R) : ↑(Subring.centralizer s) = s.centralizer
• Subring.notMem_of_notMem_closure 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] {s : Set R} {P : R} (hP : P ∉ Subring.closure s) : P ∉ s
• Subring.decidableMemCenter 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u_1} [Ring R] [DecidableEq R] [Fintype R] : DecidablePred fun x => x ∈ Subring.center R
• Subring.eq_top_iff' 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] (A : Subring R) : A = ⊤ ↔ ∀ (x : R), x ∈ A
• Subring.center_prod 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] : Subring.center (R × S) = (Subring.center R).prod (Subring.center S)
• Subring.closure_insert_natCast 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] (n : ℕ) (s : Set R) : Subring.closure (insert (↑n) s) = Subring.closure s
• Subring.closure_singleton_natCast 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] (n : ℕ) : Subring.closure {↑n} = ⊥
• Subring.center_le_centralizer 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u_1} [Ring R] (s : Set R) : Subring.center R ≤ Subring.centralizer s
• Subring.closure_insert_one 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] (s : Set R) : Subring.closure (insert 1 s) = Subring.closure s
• Subring.closure_insert_zero 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] (s : Set R) : Subring.closure (insert 0 s) = Subring.closure s
• Subring.closure_mono 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] ⦃s t : Set R⦄ (h : s ⊆ t) : Subring.closure s ≤ Subring.closure t
• Subring.closure_singleton_one 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] : Subring.closure {1} = ⊥
• Subring.closure_singleton_zero 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] : Subring.closure {0} = ⊥
• RingHom.range_eq_map 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] (f : R →+* S) : f.range = Subring.map f ⊤
• Subring.card_top 📋 Mathlib.Algebra.Ring.Subring.Basic
  (R : Type u_1) [NonAssocRing R] [Fintype R] : Fintype.card ↥⊤ = Fintype.card R
• Subring.comap_top 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] (f : R →+* S) : Subring.comap f ⊤ = ⊤
• Subring.map_bot 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] (f : R →+* S) : Subring.map f ⊥ = ⊥
• Subring.instField 📋 Mathlib.Algebra.Ring.Subring.Basic
  {K : Type u} [DivisionRing K] : Field ↥(Subring.center K)
• Subring.toSubsemiring_eq_top 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] {S : Subring R} : S.toSubsemiring = ⊤ ↔ S = ⊤
• Subring.closure_iUnion 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] {ι : Sort u_1} (s : ι → Set R) : Subring.closure (⋃ i, s i) = ⨆ i, Subring.closure (s i)
• Subring.mem_bot 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] {x : R} : x ∈ ⊥ ↔ ∃ n, ↑n = x
• Subring.toAddSubgroup_top 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] : ⊤.toAddSubgroup = ⊤
• RingHom.fintypeRange 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] [Fintype R] [DecidableEq S] (f : R →+* S) : Fintype ↥f.range
• Subring.closure_le 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] {s : Set R} {t : Subring R} : Subring.closure s ≤ t ↔ s ⊆ ↑t
• Subring.coe_iInf 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] {ι : Sort u_1} {S : ι → Subring R} : ↑(⨅ i, S i) = ⋂ i, ↑(S i)
• Subring.gi 📋 Mathlib.Algebra.Ring.Subring.Basic
  (R : Type u) [NonAssocRing R] : GaloisInsertion Subring.closure SetLike.coe
• Subring.centralizer_le 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u_1} [Ring R] (s t : Set R) (h : s ⊆ t) : Subring.centralizer t ≤ Subring.centralizer s
• Subring.toAddSubgroup_mono 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] : Monotone Subring.toAddSubgroup
• Subring.toAddSubgroup_strictMono 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] : StrictMono Subring.toAddSubgroup
• Subring.closure_union 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] (s t : Set R) : Subring.closure (s ∪ t) = Subring.closure s ⊔ Subring.closure t
• Subring.gc_map_comap 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] (f : R →+* S) : GaloisConnection (Subring.map f) (Subring.comap f)
• Subring.map_comap_eq 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] (f : R →+* S) (t : Subring S) : Subring.map f (Subring.comap f t) = t ⊓ f.range
• Subring.range_subtype 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] (s : Subring R) : s.subtype.range = s
• Subring.centralizer_eq_top_iff_subset 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u_1} [Ring R] {s : Set R} : Subring.centralizer s = ⊤ ↔ s ⊆ ↑(Subring.center R)
• Subring.closure_eq_of_le 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] {s : Set R} {t : Subring R} (h₁ : s ⊆ ↑t) (h₂ : t ≤ Subring.closure s) : Subring.closure s = t
• Subring.coe_inf 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] (p p' : Subring R) : ↑(p ⊓ p') = ↑p ∩ ↑p'
• Subring.mem_iInf 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] {ι : Sort u_1} {S : ι → Subring R} {x : R} : x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i
• Subring.toAddSubgroup_eq_top 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] {S : Subring R} : S.toAddSubgroup = ⊤ ↔ S = ⊤
• Subring.closure_le_centralizer_centralizer 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u_1} [Ring R] (s : Set R) : Subring.closure s ≤ Subring.centralizer ↑(Subring.centralizer s)
• Subring.prod_top 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] (s : Subring R) : s.prod ⊤ = Subring.comap (RingHom.fst R S) s
• Subring.top_prod 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] (s : Subring S) : ⊤.prod s = Subring.comap (RingHom.snd R S) s
• Subring.toSubmonoid_mono 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] : Monotone fun s => s.toSubmonoid
• Subring.toSubmonoid_strictMono 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] : StrictMono fun s => s.toSubmonoid
• Subring.top_prod_top 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] : ⊤.prod ⊤ = ⊤
• Subring.comap_iInf 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] {ι : Sort u_1} (f : R →+* S) (s : ι → Subring S) : Subring.comap f (iInf s) = ⨅ i, Subring.comap f (s i)
• RingHom.coe_range 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] (f : R →+* S) : ↑f.range = Set.range ⇑f
• RingHom.range_eq_top_of_surjective 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] (f : R →+* S) (hf : Function.Surjective ⇑f) : f.range = ⊤
• Subring.map_comap_eq_self 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] {f : R →+* S} {t : Subring S} (h : t ≤ f.range) : Subring.map f (Subring.comap f t) = t
• Subring.mem_closure 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] {x : R} {s : Set R} : x ∈ Subring.closure s ↔ ∀ (S : Subring R), s ⊆ ↑S → x ∈ S
• Subring.prod_mono_left 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] (t : Subring S) : Monotone fun s => s.prod t
• Subring.prod_mono_right 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] (s : Subring R) : Monotone fun t => s.prod t
• RingHom.mem_range_self 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] (f : R →+* S) (x : R) : f x ∈ f.range
• RingHom.range_eq_top 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] {f : R →+* S} : f.range = ⊤ ↔ Function.Surjective ⇑f
• RingHom.map_closure 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] (f : R →+* S) (s : Set R) : Subring.map f (Subring.closure s) = Subring.closure (⇑f '' s)
• Subring.comap_inf 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] (s t : Subring S) (f : R →+* S) : Subring.comap f (s ⊓ t) = Subring.comap f s ⊓ Subring.comap f t
• Subring.comap_map_eq_self_of_injective 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] {f : R →+* S} (hf : Function.Injective ⇑f) (s : Subring R) : Subring.comap f (Subring.map f s) = s
• Subring.map_comap_eq_self_of_surjective 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] {f : R →+* S} (hf : Function.Surjective ⇑f) (t : Subring S) : Subring.map f (Subring.comap f t) = t
• RingHom.map_range 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} {T : Type w} [NonAssocRing R] [NonAssocRing S] [NonAssocRing T] (g : S →+* T) (f : R →+* S) : Subring.map g f.range = (g.comp f).range
• Subring.mem_center_iff 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u_1} [Ring R] {z : R} : z ∈ Subring.center R ↔ ∀ (g : R), g * z = z * g
• Subring.mem_sInf 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] {S : Set (Subring R)} {x : R} : x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p
• Subring.mem_inf 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] {p p' : Subring R} {x : R} : x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'
• RingHom.mem_range 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] {f : R →+* S} {y : S} : y ∈ f.range ↔ ∃ x, f x = y
• Subring.list_sum_mem 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] (s : Subring R) {l : List R} : (∀ x ∈ l, x ∈ s) → l.sum ∈ s
• Subring.comap_comap 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} {T : Type w} [NonAssocRing R] [NonAssocRing S] [NonAssocRing T] (s : Subring T) (g : S →+* T) (f : R →+* S) : Subring.comap f (Subring.comap g s) = Subring.comap (g.comp f) s
• Subring.map_le_iff_le_comap 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] {f : R →+* S} {s : Subring R} {t : Subring S} : Subring.map f s ≤ t ↔ s ≤ Subring.comap f t
• Subring.map_map 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} {T : Type w} [NonAssocRing R] [NonAssocRing S] [NonAssocRing T] (s : Subring R) (g : S →+* T) (f : R →+* S) : Subring.map g (Subring.map f s) = Subring.map (g.comp f) s
• Subring.multiset_sum_mem 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u_1} [Ring R] (s : Subring R) (m : Multiset R) : (∀ a ∈ m, a ∈ s) → m.sum ∈ s
• Subring.coe_comap 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] (s : Subring S) (f : R →+* S) : ↑(Subring.comap f s) = ⇑f ⁻¹' ↑s
• Subring.coe_map 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] (f : R →+* S) (s : Subring R) : ↑(Subring.map f s) = ⇑f '' ↑s
• RingHom.closure_preimage_le 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] (f : R →+* S) (s : Set S) : Subring.closure (⇑f ⁻¹' s) ≤ Subring.comap f (Subring.closure s)
• Subring.closure_preimage_le 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] (f : R →+* S) (s : Set S) : Subring.closure (⇑f ⁻¹' s) ≤ Subring.comap f (Subring.closure s)
• Subring.comap_center_le_center 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] {F : Type u_1} [FunLike F R S] [RingHomClass F R S] {f : F} (hf : Function.Injective ⇑f) : Subring.comap (↑f) (Subring.center S) ≤ Subring.center R
• Subring.map_center_le_center 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] {F : Type u_1} [FunLike F R S] [RingHomClass F R S] {f : F} (hf : Function.Surjective ⇑f) : Subring.map (↑f) (Subring.center R) ≤ Subring.center S
• Subring.map_iSup 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] {ι : Sort u_1} (f : R →+* S) (s : ι → Subring R) : Subring.map f (iSup s) = ⨆ i, Subring.map f (s i)
• Subring.mem_centralizer_iff 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u_1} [Ring R] {s : Set R} {z : R} : z ∈ Subring.centralizer s ↔ ∀ g ∈ s, g * z = z * g
• Subring.coe_sInf 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] (S : Set (Subring R)) : ↑(sInf S) = ⋂ s ∈ S, ↑s
• Subring.closure_sUnion 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] (s : Set (Set R)) : Subring.closure (⋃₀ s) = ⨆ t ∈ s, Subring.closure t
• Subring.coe_prod 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] (s : Subring R) (t : Subring S) : ↑(s.prod t) = ↑s ×ˢ ↑t
• Subring.list_prod_mem 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u_1} [Ring R] (s : Subring R) {l : List R} : (∀ x ∈ l, x ∈ s) → l.prod ∈ s
• Subring.mem_comap 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] {s : Subring S} {f : R →+* S} {x : R} : x ∈ Subring.comap f s ↔ f x ∈ s
• Subring.multiset_prod_mem 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u_1} [CommRing R] (s : Subring R) (m : Multiset R) : (∀ a ∈ m, a ∈ s) → m.prod ∈ s
• Subring.sum_mem 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u_1} [Ring R] (s : Subring R) {ι : Type u_2} {t : Finset ι} {f : ι → R} (h : ∀ c ∈ t, f c ∈ s) : ∑ i ∈ t, f i ∈ s
• Subring.coe_iSup_of_directed 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] {ι : Sort u_1} [hι : Nonempty ι] {S : ι → Subring R} (hS : Directed (fun x1 x2 => x1 ≤ x2) S) : ↑(⨆ i, S i) = ⋃ i, ↑(S i)
• Subring.map_iInf 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] {ι : Sort u_1} [Nonempty ι] (f : R →+* S) (hf : Function.Injective ⇑f) (s : ι → Subring R) : Subring.map f (iInf s) = ⨅ i, Subring.map f (s i)
• RingHom.rangeRestrict 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] (f : R →+* S) : R →+* ↥f.range
• Subring.closureCommRingOfComm 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u_1} [Ring R] {s : Set R} (hcomm : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x) : CommRing ↥(Subring.closure s)
• Subring.map_sup 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] (s t : Subring R) (f : R →+* S) : Subring.map f (s ⊔ t) = Subring.map f s ⊔ Subring.map f t
• Subring.map_inf 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] (s t : Subring R) (f : R →+* S) (hf : Function.Injective ⇑f) : Subring.map f (s ⊓ t) = Subring.map f s ⊓ Subring.map f t
• Subring.mem_map 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] {f : R →+* S} {s : Subring R} {y : S} : y ∈ Subring.map f s ↔ ∃ x ∈ s, f x = y
• Subring.prod_mem 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u_1} [CommRing R] (s : Subring R) {ι : Type u_2} {t : Finset ι} {f : ι → R} (h : ∀ c ∈ t, f c ∈ s) : ∏ i ∈ t, f i ∈ s
• Subring.mem_iSup_of_directed 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] {ι : Sort u_1} [hι : Nonempty ι] {S : ι → Subring R} (hS : Directed (fun x1 x2 => x1 ≤ x2) S) {x : R} : x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i
• Subring.comap_map_eq_self 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] {f : R →+* S} {s : Subring R} (h : ⇑f ⁻¹' {0} ⊆ ↑s) : Subring.comap f (Subring.map f s) = s
• Subring.map_center_eq 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] {F : Type u_1} [EquivLike F R S] [RingEquivClass F R S] (f : F) : Subring.map (↑f) (Subring.center R) = Subring.center S
• Subring.mem_closure_iff 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] {s : Set R} {x : R} : x ∈ Subring.closure s ↔ x ∈ AddSubgroup.closure ↑(Submonoid.closure s)
• Subring.mem_prod 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] {s : Subring R} {t : Subring S} {p : R × S} : p ∈ s.prod t ↔ p.1 ∈ s ∧ p.2 ∈ t
• RingHom.mem_eqLocus 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] {S : Type v} [Semiring S] {f g : R →+* S} {x : R} : x ∈ f.eqLocus g ↔ f x = g x
• RingHom.eq_of_eqOn_set_top 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] {S : Type v} [Semiring S] {f g : R →+* S} (h : Set.EqOn ⇑f ⇑g ↑⊤) : f = g
• RingHom.eq_of_eqOn_set_dense 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] {S : Type v} [Semiring S] {s : Set R} (hs : Subring.closure s = ⊤) {f g : R →+* S} (h : Set.EqOn (⇑f) (⇑g) s) : f = g
• Subring.mem_closure_image_of 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] (f : R →+* S) {s : Set R} {x : R} (hx : x ∈ Subring.closure s) : f x ∈ Subring.closure (⇑f '' s)
• Subring.comap_map_eq 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] (f : R →+* S) (s : Subring R) : Subring.comap f (Subring.map f s) = s ⊔ Subring.closure (⇑f ⁻¹' {0})

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 ce5dd8c