Loogle!

Result

Found 19 declarations mentioning Submodule, LinearEquiv, and Function.Injective.

• Submodule.equivMapOfInjective 📋 Mathlib.Algebra.Module.Submodule.Map
  {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) (i : Function.Injective ⇑f) (p : Submodule R M) : ↥p ≃ₛₗ[σ₁₂] ↥(Submodule.map f p)
• Submodule.coe_equivMapOfInjective_apply 📋 Mathlib.Algebra.Module.Submodule.Map
  {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) (i : Function.Injective ⇑f) (p : Submodule R M) (x : ↥p) : ↑((Submodule.equivMapOfInjective f i p) x) = f ↑x
• Submodule.map_equivMapOfInjective_symm_apply 📋 Mathlib.Algebra.Module.Submodule.Map
  {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) (i : Function.Injective ⇑f) (p : Submodule R M) (x : ↥(Submodule.map f p)) : f ↑((Submodule.equivMapOfInjective f i p).symm x) = ↑x
• LinearEquiv.ofInjective 📋 Mathlib.Algebra.Module.Submodule.Equiv
  {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} (f : M →ₛₗ[σ₁₂] M₂) [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (h : Function.Injective ⇑f) : M ≃ₛₗ[σ₁₂] ↥(LinearMap.range f)
• LinearEquiv.ofInjective.congr_simp 📋 Mathlib.Algebra.Module.Submodule.Equiv
  {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} (f : M →ₛₗ[σ₁₂] M₂) [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (h : Function.Injective ⇑f) : LinearEquiv.ofInjective f h = LinearEquiv.ofInjective f h
• Submodule.comap_equiv_self_of_inj_of_le 📋 Mathlib.Algebra.Module.Submodule.Equiv
  {R : Type u_1} {M : Type u_5} {N : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {f : M →ₗ[R] N} {p : Submodule R N} (hf : Function.Injective ⇑f) (h : p ≤ LinearMap.range f) : ↥(Submodule.comap f p) ≃ₗ[R] ↥p
• LinearEquiv.ofInjective_apply 📋 Mathlib.Algebra.Module.Submodule.Equiv
  {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} (f : M →ₛₗ[σ₁₂] M₂) [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {h : Function.Injective ⇑f} (x : M) : ↑((LinearEquiv.ofInjective f h) x) = f x
• LinearEquiv.ofInjective_symm_apply 📋 Mathlib.Algebra.Module.Submodule.Equiv
  {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} (f : M →ₛₗ[σ₁₂] M₂) [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {h : Function.Injective ⇑f} (x : ↥(LinearMap.range f)) : f ((LinearEquiv.ofInjective f h).symm x) = ↑x
• Submodule.comap_equiv_self_of_inj_of_le_apply 📋 Mathlib.Algebra.Module.Submodule.Equiv
  {R : Type u_1} {M : Type u_5} {N : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {f : M →ₗ[R] N} {p : Submodule R N} (hf : Function.Injective ⇑f) (h : p ≤ LinearMap.range f) (a✝ : ↥(Submodule.comap f p)) : (Submodule.comap_equiv_self_of_inj_of_le hf h) a✝ = (LinearMap.codRestrict p (f ∘ₗ (Submodule.comap f p).subtype) ⋯) a✝
• iSupIndep_of_dfinsupp_lsum_injective 📋 Mathlib.LinearAlgebra.DFinsupp
  {ι : Type u_1} {R : Type u_3} {N : Type u_6} [DecidableEq ι] [Semiring R] [AddCommMonoid N] [Module R N] (p : ι → Submodule R N) (h : Function.Injective ⇑((DFinsupp.lsum ℕ) fun i => (p i).subtype)) : iSupIndep p
• iSupIndep.dfinsupp_lsum_injective 📋 Mathlib.LinearAlgebra.DFinsupp
  {ι : Type u_1} {R : Type u_3} {N : Type u_6} [DecidableEq ι] [Ring R] [AddCommGroup N] [Module R N] {p : ι → Submodule R N} (h : iSupIndep p) : Function.Injective ⇑((DFinsupp.lsum ℕ) fun i => (p i).subtype)
• iSupIndep_iff_dfinsupp_lsum_injective 📋 Mathlib.LinearAlgebra.DFinsupp
  {ι : Type u_1} {R : Type u_3} {N : Type u_6} [DecidableEq ι] [Ring R] [AddCommGroup N] [Module R N] (p : ι → Submodule R N) : iSupIndep p ↔ Function.Injective ⇑((DFinsupp.lsum ℕ) fun i => (p i).subtype)
• LinearMap.rTensor_injective_iff_subtype 📋 Mathlib.RingTheory.Flat.Basic
  {R : Type u} {M : Type v} {N : Type u_1} {P : Type u_2} {Q : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [AddCommMonoid Q] [Module R Q] {f : N →ₗ[R] P} (hf : Function.Injective ⇑f) (e : P ≃ₗ[R] Q) : Function.Injective ⇑(LinearMap.rTensor M f) ↔ Function.Injective ⇑(LinearMap.rTensor M (LinearMap.range (↑e ∘ₗ f)).subtype)
• lequivProdOfRightSplitExact 📋 Mathlib.Algebra.Category.ModuleCat.Biproducts
  {R : Type u} {A : Type uA} {M : Type uM} {B : Type uB} [Ring R] [AddCommGroup A] [AddCommGroup B] [AddCommGroup M] [Module R A] [Module R B] [Module R M] {j : A →ₗ[R] M} {g : M →ₗ[R] B} {f : B →ₗ[R] M} (hj : Function.Injective ⇑j) (exac : LinearMap.range j = LinearMap.ker g) (h : g ∘ₗ f = LinearMap.id) : (A × B) ≃ₗ[R] M
• PerfectPairing.restrictScalars 📋 Mathlib.LinearAlgebra.PerfectPairing.Restrict
  {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (p : M →ₗ[R] N →ₗ[R] R) [p.IsPerfPair] {S : Type u_4} {M' : Type u_5} {N' : Type u_6} [CommRing S] [Algebra S R] [Module S M] [Module S N] [IsScalarTower S R M] [IsScalarTower S R N] [NoZeroSMulDivisors S R] [Nontrivial R] [AddCommGroup M'] [Module S M'] [AddCommGroup N'] [Module S N'] (i : M' →ₗ[S] M) (j : N' →ₗ[S] N) (hi : Function.Injective ⇑i) (hj : Function.Injective ⇑j) (hM : Submodule.span R ↑(LinearMap.range i) = ⊤) (hN : Submodule.span R ↑(LinearMap.range j) = ⊤) (h₁ : ∀ (g : Module.Dual S N'), ∃ m, ↑S (p.toPerfPair (i m)) ∘ₗ j = Algebra.linearMap S R ∘ₗ g) (h₂ : ∀ (g : Module.Dual S M'), ∃ n, ↑S (p.flip.toPerfPair (j n)) ∘ₗ i = Algebra.linearMap S R ∘ₗ g) (hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap S R).range) : PerfectPairing S M' N'
• LinearMap.IsPerfPair.restrictScalars 📋 Mathlib.LinearAlgebra.PerfectPairing.Restrict
  {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (p : M →ₗ[R] N →ₗ[R] R) [p.IsPerfPair] {S : Type u_4} {M' : Type u_5} {N' : Type u_6} [CommRing S] [Algebra S R] [Module S M] [Module S N] [IsScalarTower S R M] [IsScalarTower S R N] [NoZeroSMulDivisors S R] [Nontrivial R] [AddCommGroup M'] [Module S M'] [AddCommGroup N'] [Module S N'] (i : M' →ₗ[S] M) (j : N' →ₗ[S] N) (hi : Function.Injective ⇑i) (hj : Function.Injective ⇑j) (hM : Submodule.span R ↑(LinearMap.range i) = ⊤) (hN : Submodule.span R ↑(LinearMap.range j) = ⊤) (h₁ : ∀ (g : Module.Dual S N'), ∃ m, ↑S (p.toPerfPair (i m)) ∘ₗ j = Algebra.linearMap S R ∘ₗ g) (h₂ : ∀ (g : Module.Dual S M'), ∃ n, ↑S (p.flip.toPerfPair (j n)) ∘ₗ i = Algebra.linearMap S R ∘ₗ g) (hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap S R).range) : (i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp).IsPerfPair
• ContinuousLinearMap.equivRange_symm_toLinearEquiv 📋 Mathlib.Analysis.Normed.Operator.Banach
  {𝕜 : Type u_1} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜' F] {σ' : 𝕜' →+* 𝕜} [RingHomInvPair σ σ'] [RingHomIsometric σ] [RingHomIsometric σ'] [CompleteSpace F] [CompleteSpace E] [RingHomInvPair σ' σ] {f : E →SL[σ] F} (hinj : Function.Injective ⇑f) (hclo : IsClosed (Set.range ⇑f)) : (ContinuousLinearMap.equivRange hinj hclo).symm = (LinearEquiv.ofInjective (↑f) hinj).symm
• AffineSubspace.linear_equivMapOfInjective 📋 Mathlib.Analysis.Normed.Affine.Isometry
  {𝕜 : Type u_1} {V₁ : Type u_3} {V₂ : Type u_5} {P₁ : Type u_8} {P₂ : Type u_11} [NormedField 𝕜] [SeminormedAddCommGroup V₁] [NormedSpace 𝕜 V₁] [PseudoMetricSpace P₁] [NormedAddTorsor V₁ P₁] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂] [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] (E : AffineSubspace 𝕜 P₁) [Nonempty ↥E] (φ : P₁ →ᵃ[𝕜] P₂) (hφ : Function.Injective ⇑φ) : (E.equivMapOfInjective φ hφ).linear = (Submodule.equivMapOfInjective φ.linear ⋯ E.direction).trans (LinearEquiv.ofEq (Submodule.map φ.linear E.direction) (AffineSubspace.map φ E).direction ⋯)
• Submodule.equivMapOfInjective.congr_simp 📋 Mathlib.LinearAlgebra.LinearDisjoint
  {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) (i : Function.Injective ⇑f) (p : Submodule R M) : Submodule.equivMapOfInjective f i p = Submodule.equivMapOfInjective f i p

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 6ff4759 serving mathlib revision 0bf098c