Loogle!

Result

Found 18 declarations mentioning NonUnitalStarSubalgebra.map.

• NonUnitalStarSubalgebra.map 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] (f : F) (S : NonUnitalStarSubalgebra R A) : NonUnitalStarSubalgebra R B
• NonUnitalStarSubalgebra.map_injective 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] {f : F} (hf : Function.Injective ⇑f) : Function.Injective (NonUnitalStarSubalgebra.map f)
• NonUnitalStarSubalgebra.map_toNonUnitalSubalgebra 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] {S : NonUnitalStarSubalgebra R A} {f : F} : (NonUnitalStarSubalgebra.map f S).toNonUnitalSubalgebra = NonUnitalSubalgebra.map f S.toNonUnitalSubalgebra
• NonUnitalStarSubalgebra.coe_map 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] (S : NonUnitalStarSubalgebra R A) (f : F) : ↑(NonUnitalStarSubalgebra.map f S) = ⇑f '' ↑S
• NonUnitalStarSubalgebra.mem_map 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] {S : NonUnitalStarSubalgebra R A} {f : F} {y : B} : y ∈ NonUnitalStarSubalgebra.map f S ↔ ∃ x ∈ S, f x = y
• NonUnitalStarSubalgebra.gc_map_comap 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] (f : F) : GaloisConnection (NonUnitalStarSubalgebra.map f) (NonUnitalStarSubalgebra.comap f)
• NonUnitalStarSubalgebra.map_id 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] (S : NonUnitalStarSubalgebra R A) : NonUnitalStarSubalgebra.map (NonUnitalStarAlgHom.id R A) S = S
• NonUnitalStarSubalgebra.map_mono 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] {S₁ S₂ : NonUnitalStarSubalgebra R A} {f : F} : S₁ ≤ S₂ → NonUnitalStarSubalgebra.map f S₁ ≤ NonUnitalStarSubalgebra.map f S₂
• NonUnitalStarSubalgebra.map_le 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] {S : NonUnitalStarSubalgebra R A} {f : F} {U : NonUnitalStarSubalgebra R B} : NonUnitalStarSubalgebra.map f S ≤ U ↔ S ≤ NonUnitalStarSubalgebra.comap f U
• NonUnitalStarAlgHom.range_comp 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} {B : Type w} {C : Type w'} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [NonUnitalNonAssocSemiring C] [Module R C] [Star C] (f : A →⋆ₙₐ[R] B) (g : B →⋆ₙₐ[R] C) : NonUnitalStarAlgHom.range (g.comp f) = NonUnitalStarSubalgebra.map g (NonUnitalStarAlgHom.range f)
• NonUnitalStarSubalgebra.map_map 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} {B : Type w} {C : Type w'} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [NonUnitalNonAssocSemiring C] [Module R C] [Star C] (S : NonUnitalStarSubalgebra R A) (g : B →⋆ₙₐ[R] C) (f : A →⋆ₙₐ[R] B) : NonUnitalStarSubalgebra.map g (NonUnitalStarSubalgebra.map f S) = NonUnitalStarSubalgebra.map (g.comp f) S
• NonUnitalStarAlgebra.map_top 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [NonUnitalSemiring B] [StarRing B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] (f : F) : NonUnitalStarSubalgebra.map f ⊤ = NonUnitalStarAlgHom.range f
• NonUnitalStarAlgHom.map_adjoin 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalSemiring A] [StarRing A] [Module R A] [NonUnitalSemiring B] [StarRing B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] [StarRing R] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [IsScalarTower R B B] [SMulCommClass R B B] [StarModule R B] (f : F) (s : Set A) : NonUnitalStarSubalgebra.map f (NonUnitalStarAlgebra.adjoin R s) = NonUnitalStarAlgebra.adjoin R (⇑f '' s)
• NonUnitalStarAlgHom.map_adjoin_singleton 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalSemiring A] [StarRing A] [Module R A] [NonUnitalSemiring B] [StarRing B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] [StarRing R] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [IsScalarTower R B B] [SMulCommClass R B B] [StarModule R B] (f : F) (x : A) : NonUnitalStarSubalgebra.map f (NonUnitalStarAlgebra.adjoin R {x}) = NonUnitalStarAlgebra.adjoin R {f x}
• NonUnitalStarAlgebra.map_bot 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [NonUnitalSemiring B] [StarRing B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [IsScalarTower R B B] [SMulCommClass R B B] [StarModule R B] (f : F) : NonUnitalStarSubalgebra.map f ⊥ = ⊥
• NonUnitalStarAlgebra.map_iInf 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [NonUnitalSemiring B] [StarRing B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] {ι : Sort u_1} [Nonempty ι] [IsScalarTower R B B] [SMulCommClass R B B] [StarModule R B] (f : F) (hf : Function.Injective ⇑f) (S : ι → NonUnitalStarSubalgebra R A) : NonUnitalStarSubalgebra.map f (⨅ i, S i) = ⨅ i, NonUnitalStarSubalgebra.map f (S i)
• NonUnitalStarAlgebra.map_sup 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [NonUnitalSemiring B] [StarRing B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [IsScalarTower R B B] [SMulCommClass R B B] [StarModule R B] (f : F) (S T : NonUnitalStarSubalgebra R A) : NonUnitalStarSubalgebra.map f (S ⊔ T) = NonUnitalStarSubalgebra.map f S ⊔ NonUnitalStarSubalgebra.map f T
• NonUnitalStarAlgebra.map_inf 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [NonUnitalSemiring B] [StarRing B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [IsScalarTower R B B] [SMulCommClass R B B] [StarModule R B] (f : F) (hf : Function.Injective ⇑f) (S T : NonUnitalStarSubalgebra R A) : NonUnitalStarSubalgebra.map f (S ⊓ T) = NonUnitalStarSubalgebra.map f S ⊓ NonUnitalStarSubalgebra.map f T

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 40fea08