Loogle!

Result

Found 33 declarations mentioning Subring.map.

• Subring.map_id 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [Ring R] (s : Subring R) : Subring.map (RingHom.id R) s = s
• Subring.map 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [Ring R] [Ring S] (f : R →+* S) (s : Subring R) : Subring S
• RingHom.range_eq_map 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [Ring R] [Ring S] (f : R →+* S) : f.range = Subring.map f ⊤
• Subring.map_bot 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [Ring R] [Ring S] (f : R →+* S) : Subring.map f ⊥ = ⊥
• Subring.map_comap_eq 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [Ring R] [Ring S] (f : R →+* S) (t : Subring S) : Subring.map f (Subring.comap f t) = t ⊓ f.range
• Subring.gc_map_comap 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [Ring R] [Ring S] (f : R →+* S) : GaloisConnection (Subring.map f) (Subring.comap f)
• Subring.map_comap_eq_self 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [Ring R] [Ring S] {f : R →+* S} {t : Subring S} (h : t ≤ f.range) : Subring.map f (Subring.comap f t) = t
• RingHom.map_closure 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [Ring R] [Ring S] (f : R →+* S) (s : Set R) : Subring.map f (Subring.closure s) = Subring.closure (⇑f '' s)
• Subring.comap_map_eq_self_of_injective 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [Ring R] [Ring 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} [Ring R] [Ring S] {f : R →+* S} (hf : Function.Surjective ⇑f) (t : Subring S) : Subring.map f (Subring.comap f t) = t
• Subring.map_iSup 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [Ring R] [Ring S] {ι : Sort u_1} (f : R →+* S) (s : ι → Subring R) : Subring.map f (iSup s) = ⨆ i, Subring.map f (s i)
• RingHom.map_range 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} {T : Type w} [Ring R] [Ring S] [Ring T] (g : S →+* T) (f : R →+* S) : Subring.map g f.range = (g.comp f).range
• Subring.map_le_iff_le_comap 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [Ring R] [Ring 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} [Ring R] [Ring S] [Ring T] (s : Subring R) (g : S →+* T) (f : R →+* S) : Subring.map g (Subring.map f s) = Subring.map (g.comp f) s
• Subring.coe_map 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [Ring R] [Ring S] (f : R →+* S) (s : Subring R) : ↑(Subring.map f s) = ⇑f '' ↑s
• Subring.map_sup 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [Ring R] [Ring S] (s t : Subring R) (f : R →+* S) : Subring.map f (s ⊔ t) = Subring.map f s ⊔ Subring.map f t
• Subring.map_iInf 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [Ring R] [Ring 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)
• Subring.map_inf 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [Ring R] [Ring 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} [Ring R] [Ring S] {f : R →+* S} {s : Subring R} {y : S} : y ∈ Subring.map f s ↔ ∃ x ∈ s, f x = y
• Subring.comap_map_eq_self 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [Ring R] [Ring S] {f : R →+* S} {s : Subring R} (h : ⇑f ⁻¹' {0} ⊆ ↑s) : Subring.comap f (Subring.map f s) = s
• Subring.comap_map_eq 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [Ring R] [Ring S] (f : R →+* S) (s : Subring R) : Subring.comap f (Subring.map f s) = s ⊔ Subring.closure (⇑f ⁻¹' {0})
• Subring.equivMapOfInjective 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [Ring R] [Ring S] (s : Subring R) (f : R →+* S) (hf : Function.Injective ⇑f) : ↥s ≃+* ↥(Subring.map f s)
• Subring.mem_map_equiv 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [Ring R] [Ring S] {f : R ≃+* S} {K : Subring R} {x : S} : x ∈ Subring.map (↑f) K ↔ f.symm x ∈ K
• RingEquiv.subringMap 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [Ring R] [Ring S] {s : Subring R} (e : R ≃+* S) : ↥s ≃+* ↥(Subring.map e.toRingHom s)
• Subring.comap_equiv_eq_map_symm 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [Ring R] [Ring S] (f : R ≃+* S) (K : Subring S) : Subring.comap (↑f) K = Subring.map (↑f.symm) K
• Subring.map_equiv_eq_comap_symm 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [Ring R] [Ring S] (f : R ≃+* S) (K : Subring R) : Subring.map (↑f) K = Subring.comap (↑f.symm) K
• Subring.coe_equivMapOfInjective_apply 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [Ring R] [Ring S] (s : Subring R) (f : R →+* S) (hf : Function.Injective ⇑f) (x : ↥s) : ↑((s.equivMapOfInjective f hf) x) = f ↑x
• Subring.pointwise_smul_def 📋 Mathlib.Algebra.Ring.Subring.Pointwise
  {M : Type u_1} {R : Type u_2} [Monoid M] [Ring R] [MulSemiringAction M R] {a : M} (S : Subring R) : a • S = Subring.map (MulSemiringAction.toRingHom M R a) S
• LocalSubring.map_toSubring 📋 Mathlib.RingTheory.LocalRing.LocalSubring
  {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Nontrivial S] (f : R →+* S) (s : LocalSubring R) : (LocalSubring.map f s).toSubring = Subring.map f s.toSubring
• LocalSubring.range_toSubring 📋 Mathlib.RingTheory.LocalRing.LocalSubring
  {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsLocalRing R] [Nontrivial S] (f : R →+* S) : (LocalSubring.range f).toSubring = (Subring.map f ⊤).copy (Set.range ⇑f) ⋯
• instIsLocalRingSubtypeMemSubringMapOfNontrivial 📋 Mathlib.RingTheory.LocalRing.LocalSubring
  {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Nontrivial S] (f : R →+* S) (s : Subring R) [IsLocalRing ↥s] : IsLocalRing ↥(Subring.map f s)
• LaurentSeries.powerSeries_ext_subring 📋 Mathlib.RingTheory.LaurentSeries
  (K : Type u_2) [Field K] : Subring.map (LaurentSeries.LaurentSeriesRingEquiv K).toRingHom (LaurentSeries.powerSeries_as_subring K) = (IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers (RatFunc K) (Polynomial.idealX K)).toSubring
• LaurentSeries.powerSeriesEquivSubring_apply 📋 Mathlib.RingTheory.LaurentSeries
  (K : Type u_2) [Field K] (f : PowerSeries K) : (LaurentSeries.powerSeriesEquivSubring K) f = ⟨(HahnSeries.ofPowerSeries ℤ K) f, ⋯⟩

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.

This is Loogle revision 19971e9 serving mathlib revision bce1d65