Loogle!

Result

Found 3532 declarations mentioning Function.Injective. Of these, 23 have a name containing "rtensor".

LinearMap.lTensor_inj_iff_rTensor_inj 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
{R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) : Function.Injective ⇑(LinearMap.lTensor M f) ↔ Function.Injective ⇑(LinearMap.rTensor M f)
rTensor_injective_iff_lcomp_surjective 📋 Mathlib.Algebra.Module.CharacterModule
{R : Type uR} [CommRing R] {A : Type uA} [AddCommGroup A] {A' : Type u_1} [AddCommGroup A'] {B : Type uB} [AddCommGroup B] [Module R A] [Module R A'] [Module R B] {f : A →ₗ[R] A'} : Function.Injective ⇑(LinearMap.rTensor B f) ↔ Function.Surjective ⇑(LinearMap.lcomp R (CharacterModule B) f)
Module.Flat.rTensor_preserves_injective_linearMap 📋 Mathlib.RingTheory.Flat.Basic
{R : Type u} {M : Type v} {N : Type u_1} {P : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module.Flat R M] (f : N →ₗ[R] P) (hf : Function.Injective ⇑f) : Function.Injective ⇑(LinearMap.rTensor M f)
Module.Flat.iff_rTensor_preserves_injective_linearMapₛ 📋 Mathlib.RingTheory.Flat.Basic
{R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] [Small.{v', u} R] : Module.Flat R M ↔ ∀ ⦃N N' : Type v'⦄ [inst : AddCommMonoid N] [inst_1 : AddCommMonoid N'] [inst_2 : Module R N] [inst_3 : Module R N'] (f : N →ₗ[R] N'), Function.Injective ⇑f → Function.Injective ⇑(LinearMap.rTensor M f)
Module.Flat.iff_rTensor_preserves_injective_linearMap 📋 Mathlib.RingTheory.Flat.Basic
{R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] : Module.Flat R M ↔ ∀ ⦃N N' : Type (max u v)⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N] [inst_3 : Module R N'] (f : N →ₗ[R] N'), Function.Injective ⇑f → Function.Injective ⇑(LinearMap.rTensor M f)
Module.Flat.iff_rTensor_preserves_injective_linearMap' 📋 Mathlib.RingTheory.Flat.Basic
{R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Small.{v', u} R] : Module.Flat R M ↔ ∀ ⦃N N' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N] [inst_3 : Module R N'] (f : N →ₗ[R] N'), Function.Injective ⇑f → Function.Injective ⇑(LinearMap.rTensor M f)
Module.Flat.iff_rTensor_injectiveₛ 📋 Mathlib.RingTheory.Flat.Basic
{R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] : Module.Flat R M ↔ ∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P), Function.Injective ⇑(LinearMap.rTensor M N.subtype)
LinearMap.rTensor_injective_of_fg 📋 Mathlib.RingTheory.Flat.Basic
{R : Type u} {M : Type v} {N : Type u_1} {P : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] {f : N →ₗ[R] P} (h : ∀ (N' : Submodule R N) (P' : Submodule R P), N'.FG → P'.FG → ∀ (h : N' ≤ Submodule.comap f P'), Function.Injective ⇑(LinearMap.rTensor M (f.restrict h))) : Function.Injective ⇑(LinearMap.rTensor M f)
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)
TensorProduct.rTensor_injective_of_forall_vanishesTrivially 📋 Mathlib.LinearAlgebra.TensorProduct.Vanishing
(R : Type u_1) [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] (hMN : ∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, ∑ i, m i ⊗ₜ[R] n i = 0 → TensorProduct.VanishesTrivially R m n) (M' : Submodule R M) : Function.Injective ⇑(LinearMap.rTensor N M'.subtype)
TensorProduct.forall_vanishesTrivially_iff_forall_rTensor_injective 📋 Mathlib.LinearAlgebra.TensorProduct.Vanishing
(R : Type u_1) [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] : (∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, ∑ i, m i ⊗ₜ[R] n i = 0 → TensorProduct.VanishesTrivially R m n) ↔ ∀ (M' : Submodule R M), Function.Injective ⇑(LinearMap.rTensor N M'.subtype)
TensorProduct.forall_vanishesTrivially_iff_forall_fg_rTensor_injective 📋 Mathlib.LinearAlgebra.TensorProduct.Vanishing
(R : Type u_1) [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] : (∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, ∑ i, m i ⊗ₜ[R] n i = 0 → TensorProduct.VanishesTrivially R m n) ↔ ∀ (M' : Submodule R M), M'.FG → Function.Injective ⇑(LinearMap.rTensor N M'.subtype)
TensorProduct.vanishesTrivially_of_sum_tmul_eq_zero_of_rTensor_injective 📋 Mathlib.LinearAlgebra.TensorProduct.Vanishing
(R : Type u_1) [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] {ι : Type u_4} [Fintype ι] {m : ι → M} {n : ι → N} (hm : Function.Injective ⇑(LinearMap.rTensor N (Submodule.span R (Set.range m)).subtype)) (hmn : ∑ i, m i ⊗ₜ[R] n i = 0) : TensorProduct.VanishesTrivially R m n
TensorProduct.vanishesTrivially_iff_sum_tmul_eq_zero_of_rTensor_injective 📋 Mathlib.LinearAlgebra.TensorProduct.Vanishing
(R : Type u_1) [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] {ι : Type u_4} [Fintype ι] {m : ι → M} {n : ι → N} (hm : Function.Injective ⇑(LinearMap.rTensor N (Submodule.span R (Set.range m)).subtype)) : TensorProduct.VanishesTrivially R m n ↔ ∑ i, m i ⊗ₜ[R] n i = 0
TensorProduct.rTensor_injective_of_forall_fg_rTensor_injective 📋 Mathlib.LinearAlgebra.TensorProduct.Vanishing
(R : Type u_1) [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] (hMN : ∀ (M' : Submodule R M), M'.FG → Function.Injective ⇑(LinearMap.rTensor N M'.subtype)) (M' : Submodule R M) : Function.Injective ⇑(LinearMap.rTensor N M'.subtype)
Module.Flat.injective_characterModule_iff_rTensor_preserves_injective_linearMap 📋 Mathlib.RingTheory.Flat.Tensor
{R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] : Module.Injective R (CharacterModule M) ↔ ∀ ⦃N N' : Type v⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N] [inst_3 : Module R N'] (f : N →ₗ[R] N'), Function.Injective ⇑f → Function.Injective ⇑(LinearMap.rTensor M f)
Module.Flat.iff_rTensor_injective' 📋 Mathlib.RingTheory.Flat.Tensor
{R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] : Module.Flat R M ↔ ∀ (I : Ideal R), Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype I))
Module.Flat.iff_rTensor_injective 📋 Mathlib.RingTheory.Flat.Tensor
{R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] : Module.Flat R M ↔ ∀ ⦃I : Ideal R⦄, I.FG → Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype I))
lTensor_injective_of_exact_of_exact_of_rTensor_injective 📋 Mathlib.RingTheory.LocalRing.Module
{R : Type u_1} [CommRing R] {M₁ : Type u_5} {M₂ : Type u_6} {M₃ : Type u_7} {N₁ : Type u_8} {N₂ : Type u_9} {N₃ : Type u_10} [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] [AddCommGroup M₃] [Module R M₃] [AddCommGroup N₁] [Module R N₁] [AddCommGroup N₂] [Module R N₂] [AddCommGroup N₃] [Module R N₃] {f₁ : M₁ →ₗ[R] M₂} {f₂ : M₂ →ₗ[R] M₃} {g₁ : N₁ →ₗ[R] N₂} {g₂ : N₂ →ₗ[R] N₃} (hfexact : Function.Exact ⇑f₁ ⇑f₂) (hfsurj : Function.Surjective ⇑f₂) (hgexact : Function.Exact ⇑g₁ ⇑g₂) (hgsurj : Function.Surjective ⇑g₂) (hfinj : Function.Injective ⇑(LinearMap.rTensor N₃ f₁)) (hginj : Function.Injective ⇑(LinearMap.lTensor M₂ g₁)) : Function.Injective ⇑(LinearMap.lTensor M₃ g₁)
Module.free_of_maximalIdeal_rTensor_injective 📋 Mathlib.RingTheory.LocalRing.Module
{R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [IsLocalRing R] [Module.FinitePresentation R M] (H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype (IsLocalRing.maximalIdeal R)))) : Module.Free R M
Module.exists_basis_of_span_of_maximalIdeal_rTensor_injective 📋 Mathlib.RingTheory.LocalRing.Module
{R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [IsLocalRing R] [Module.FinitePresentation R M] (H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype (IsLocalRing.maximalIdeal R)))) {ι : Type u} (v : ι → M) (hv : Submodule.span R (Set.range v) = ⊤) : ∃ κ a b, ∀ (i : κ), b i = v (a i)
Module.Invertible.rTensor_injective_iff 📋 Mathlib.RingTheory.PicardGroup
{R : Type u} (M : Type v) {N : Type u_1} {P : Type u_2} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] [Module.Invertible R M] {f : N →ₗ[R] P} : Function.Injective ⇑(LinearMap.rTensor M f) ↔ Function.Injective ⇑f
Module.Invertible.rTensorInv_injective 📋 Mathlib.RingTheory.PicardGroup
{R : Type u} {M : Type v} {N : Type u_1} (P : Type u_2) (Q : Type u_3) [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (e : TensorProduct R M N ≃ₗ[R] R) : Function.Injective ⇑(Module.Invertible.rTensorInv P Q e)

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:

By constant:
🔍 Real.sin
finds all lemmas whose statement somehow mentions the sine function.
By lemma name substring:
🔍 "differ"
finds all lemmas that have "differ" somewhere in their lemma name.
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
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 0ac13cd serving mathlib revision ff5ab5e