Loogle!

Result

Found 25 declarations mentioning Subfield.map.

• Subfield.map 📋 Mathlib.Algebra.Field.Subfield.Basic
  {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing L] (f : K →+* L) (s : Subfield K) : Subfield L
• Subfield.comap_map 📋 Mathlib.Algebra.Field.Subfield.Basic
  {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing L] (f : K →+* L) (s : Subfield K) : Subfield.comap f (Subfield.map f s) = s
• RingHom.fieldRange_eq_map 📋 Mathlib.Algebra.Field.Subfield.Basic
  {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing L] (f : K →+* L) : f.fieldRange = Subfield.map f ⊤
• Subfield.map_bot 📋 Mathlib.Algebra.Field.Subfield.Basic
  {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing L] (f : K →+* L) : Subfield.map f ⊥ = ⊥
• Subfield.map_comap_eq 📋 Mathlib.Algebra.Field.Subfield.Basic
  {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing L] (f : K →+* L) (s : Subfield L) : Subfield.map f (Subfield.comap f s) = s ⊓ f.fieldRange
• Subfield.gc_map_comap 📋 Mathlib.Algebra.Field.Subfield.Basic
  {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing L] (f : K →+* L) : GaloisConnection (Subfield.map f) (Subfield.comap f)
• Subfield.map_iInf 📋 Mathlib.Algebra.Field.Subfield.Basic
  {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing L] {ι : Sort u_1} [Nonempty ι] (f : K →+* L) (s : ι → Subfield K) : Subfield.map f (iInf s) = ⨅ i, Subfield.map f (s i)
• Subfield.map_inf 📋 Mathlib.Algebra.Field.Subfield.Basic
  {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing L] (s t : Subfield K) (f : K →+* L) : Subfield.map f (s ⊓ t) = Subfield.map f s ⊓ Subfield.map f t
• Subfield.map_comap_eq_self 📋 Mathlib.Algebra.Field.Subfield.Basic
  {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing L] {f : K →+* L} {s : Subfield L} (h : s ≤ f.fieldRange) : Subfield.map f (Subfield.comap f s) = s
• Subfield.map_iSup 📋 Mathlib.Algebra.Field.Subfield.Basic
  {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing L] {ι : Sort u_1} (f : K →+* L) (s : ι → Subfield K) : Subfield.map f (iSup s) = ⨆ i, Subfield.map f (s i)
• RingHom.map_field_closure 📋 Mathlib.Algebra.Field.Subfield.Basic
  {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing L] (f : K →+* L) (s : Set K) : Subfield.map f (Subfield.closure s) = Subfield.closure (⇑f '' s)
• Subfield.map_comap_eq_self_of_surjective 📋 Mathlib.Algebra.Field.Subfield.Basic
  {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing L] {f : K →+* L} (hf : Function.Surjective ⇑f) (s : Subfield L) : Subfield.map f (Subfield.comap f s) = s
• Subfield.map_le_iff_le_comap 📋 Mathlib.Algebra.Field.Subfield.Basic
  {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing L] {f : K →+* L} {s : Subfield K} {t : Subfield L} : Subfield.map f s ≤ t ↔ s ≤ Subfield.comap f t
• RingHom.map_fieldRange 📋 Mathlib.Algebra.Field.Subfield.Basic
  {K : Type u} {L : Type v} {M : Type w} [DivisionRing K] [DivisionRing L] [DivisionRing M] (g : L →+* M) (f : K →+* L) : Subfield.map g f.fieldRange = (g.comp f).fieldRange
• Subfield.coe_map 📋 Mathlib.Algebra.Field.Subfield.Basic
  {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing L] (s : Subfield K) (f : K →+* L) : ↑(Subfield.map f s) = ⇑f '' ↑s
• Subfield.map_map 📋 Mathlib.Algebra.Field.Subfield.Basic
  {K : Type u} {L : Type v} {M : Type w} [DivisionRing K] [DivisionRing L] [DivisionRing M] (s : Subfield K) (g : L →+* M) (f : K →+* L) : Subfield.map g (Subfield.map f s) = Subfield.map (g.comp f) s
• Subfield.map_sup 📋 Mathlib.Algebra.Field.Subfield.Basic
  {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing L] (s t : Subfield K) (f : K →+* L) : Subfield.map f (s ⊔ t) = Subfield.map f s ⊔ Subfield.map f t
• Subfield.mem_map 📋 Mathlib.Algebra.Field.Subfield.Basic
  {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing L] {f : K →+* L} {s : Subfield K} {y : L} : y ∈ Subfield.map f s ↔ ∃ x ∈ s, f x = y
• IntermediateField.toSubfield_map 📋 Mathlib.FieldTheory.IntermediateField.Basic
  {K : Type u_1} {L : Type u_2} {L' : Type u_3} [Field K] [Field L] [Field L'] [Algebra K L] [Algebra K L'] (S : IntermediateField K L) (f : L →ₐ[K] L') : (IntermediateField.map f S).toSubfield = Subfield.map (↑f) S.toSubfield
• Subfield.relfinrank_comap 📋 Mathlib.FieldTheory.Relrank
  {E : Type v} [Field E] {L : Type w} [Field L] (A : Subfield E) (f : L →+* E) (B : Subfield L) : (Subfield.comap f A).relfinrank B = A.relfinrank (Subfield.map f B)
• Subfield.relfinrank_map_map 📋 Mathlib.FieldTheory.Relrank
  {E : Type v} [Field E] {L : Type w} [Field L] (A B : Subfield E) (f : E →+* L) : (Subfield.map f A).relfinrank (Subfield.map f B) = A.relfinrank B
• Subfield.relrank_comap 📋 Mathlib.FieldTheory.Relrank
  {E : Type v} [Field E] (A : Subfield E) {L : Type v} [Field L] (f : L →+* E) (B : Subfield L) : (Subfield.comap f A).relrank B = A.relrank (Subfield.map f B)
• Subfield.relrank_map_map 📋 Mathlib.FieldTheory.Relrank
  {E : Type v} [Field E] (A B : Subfield E) {L : Type v} [Field L] (f : E →+* L) : (Subfield.map f A).relrank (Subfield.map f B) = A.relrank B
• Subfield.lift_relrank_comap 📋 Mathlib.FieldTheory.Relrank
  {E : Type v} [Field E] {L : Type w} [Field L] (A : Subfield E) (f : L →+* E) (B : Subfield L) : Cardinal.lift.{v, w} ((Subfield.comap f A).relrank B) = Cardinal.lift.{w, v} (A.relrank (Subfield.map f B))
• Subfield.lift_relrank_map_map 📋 Mathlib.FieldTheory.Relrank
  {E : Type v} [Field E] {L : Type w} [Field L] (A B : Subfield E) (f : E →+* L) : Cardinal.lift.{v, w} ((Subfield.map f A).relrank (Subfield.map f B)) = Cardinal.lift.{w, v} (A.relrank B)

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