Loogle!

Result

Found 50 declarations mentioning LinearMap.range and Submodule.span.

• LinearMap.range_toSpanSingleton 📋 Mathlib.LinearAlgebra.Span.Basic
  {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (x : M) : (LinearMap.toSpanSingleton R M x).range = R ∙ x
• LinearMap.span_singleton_eq_range 📋 Mathlib.LinearAlgebra.Span.Basic
  (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] (x : M) : R ∙ x = (LinearMap.toSpanSingleton R M x).range
• Fintype.range_linearCombination 📋 Mathlib.LinearAlgebra.Finsupp.LinearCombination
  {α : Type u_1} {M : Type u_2} (R : Type u_3) [Fintype α] [Semiring R] [AddCommMonoid M] [Module R M] (v : α → M) : (Fintype.linearCombination R v).range = Submodule.span R (Set.range v)
• Finsupp.range_linearCombination 📋 Mathlib.LinearAlgebra.Finsupp.LinearCombination
  {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {v : α → M} : (Finsupp.linearCombination R v).range = Submodule.span R (Set.range v)
• Finsupp.span_eq_range_linearCombination 📋 Mathlib.LinearAlgebra.Finsupp.LinearCombination
  {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (s : Set M) : Submodule.span R s = (Finsupp.linearCombination R Subtype.val).range
• Finsupp.linearCombinationOn_range 📋 Mathlib.LinearAlgebra.Finsupp.LinearCombination
  {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {v : α → M} (s : Set α) : (Finsupp.linearCombinationOn α M R v s).range = ⊤
• Module.Basis.constr_range 📋 Mathlib.LinearAlgebra.Basis.Defs
  {M' : Type u_7} [AddCommMonoid M'] {ι : Type u_10} {R : Type u_11} {M : Type u_12} [Semiring R] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) [Module R M'] (S : Type u_13) [Semiring S] [Module S M'] [SMulCommClass R S M'] {f : ι → M'} : ((b.constr S) f).range = Submodule.span R (Set.range f)
• LinearIndependent.repr_range 📋 Mathlib.LinearAlgebra.LinearIndependent.Defs
  {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] (hv : LinearIndependent R v) : hv.repr.range = ⊤
• LinearIndependent.linearCombinationEquiv_symm_apply 📋 Mathlib.LinearAlgebra.LinearIndependent.Defs
  {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] (hv : LinearIndependent R v) (a✝ : ↥(Submodule.span R (Set.range v))) : hv.linearCombinationEquiv.symm a✝ = ((LinearEquiv.ofInjective (LinearMap.codRestrict (Submodule.span R (Set.range v)) (Finsupp.linearCombination R v) ⋯) ⋯).toEquiv.trans (LinearEquiv.ofTop (LinearMap.codRestrict (Submodule.span R (Set.range v)) (Finsupp.linearCombination R v) ⋯).range ⋯).toEquiv).invFun a✝
• Submodule.span_preimage_eq 📋 Mathlib.LinearAlgebra.Quotient.Basic
  {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {R₂ : Type u_3} {M₂ : Type u_4} [Ring R₂] [AddCommGroup M₂] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} {s : Set M₂} (h₀ : s.Nonempty) (h₁ : s ⊆ ↑f.range) : Submodule.span R (⇑f ⁻¹' s) = Submodule.comap f (Submodule.span R₂ s)
• Finsupp.range_lmapDomain 📋 Mathlib.LinearAlgebra.Finsupp.Span
  {α : Type u_1} {R : Type u_5} [Semiring R] {β : Type u_7} (u : α → β) : (Finsupp.lmapDomain R R u).range = Submodule.span R (Set.range fun x => fun₀ | u x => 1)
• Finsupp.isCompl_range_lmapDomain_span 📋 Mathlib.LinearAlgebra.Finsupp.VectorSpace
  {R : Type u_1} {ι : Type u_3} [Semiring R] {α : Type u_4} {β : Type u_5} {u : α → ι} {v : β → ι} (huv : IsCompl (Set.range u) (Set.range v)) : IsCompl (Finsupp.lmapDomain R R u).range (Submodule.span R (Set.range fun x => fun₀ | v x => 1))
• Module.range_piEquiv 📋 Mathlib.LinearAlgebra.StdBasis
  (ι : Type u_1) (R : Type u_2) (M : Type u_3) [Finite ι] [CommSemiring R] [AddCommMonoid M] [Module R M] (v : ι → M) : ((Module.piEquiv ι R M) v).range = Submodule.span R (Set.range v)
• TensorProduct.map_range_eq_span_tmul 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_7} {N : Type u_8} {P : Type u_9} {Q : Type u_10} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : (TensorProduct.map f g).range = Submodule.span R {t | ∃ m n, f m ⊗ₜ[R] g n = t}
• TensorProduct.range_map_eq_span_tmul 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_7} {N : Type u_8} {P : Type u_9} {Q : Type u_10} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : (TensorProduct.map f g).range = Submodule.span R {t | ∃ m n, f m ⊗ₜ[R] g n = t}
• Ideal.range_finsuppTotal 📋 Mathlib.RingTheory.Ideal.Operations
  {ι : Type u_1} {M : Type u_2} [AddCommGroup M] {R : Type u_3} [CommRing R] [Module R M] (I : Ideal R) {v : ι → M} : (Ideal.finsuppTotal ι M I v).range = I • Submodule.span R (Set.range v)
• range_vecMulLinear 📋 Mathlib.LinearAlgebra.Matrix.ToLin
  {R : Type u_1} [Semiring R] {m : Type u_3} {n : Type u_4} [Fintype m] (M : Matrix m n R) : M.vecMulLinear.range = Submodule.span R (Set.range M.row)
• Matrix.range_mulVecLin 📋 Mathlib.LinearAlgebra.Matrix.ToLin
  {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [Fintype n] (M : Matrix m n R) : M.mulVecLin.range = Submodule.span R (Set.range M.col)
• Matrix.range_toLin' 📋 Mathlib.LinearAlgebra.Matrix.ToLin
  {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [DecidableEq n] [Fintype n] (M : Matrix m n R) : (Matrix.toLin' M).range = Submodule.span R (Set.range M.col)
• LinearMap.range_liftBaseChange 📋 Mathlib.RingTheory.TensorProduct.Basic
  {R : Type u_1} {M : Type u_2} {N : Type u_3} (A : Type u_4) [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module A N] [IsScalarTower R A N] (l : M →ₗ[R] N) : (LinearMap.liftBaseChange A l).range = Submodule.span A ↑l.range
• LinearMap.range_smulRight_apply_of_surjective 📋 Mathlib.Algebra.Module.LinearMap.DivisionRing
  {R : Type u_1} {M : Type u_2} {M₁ : Type u_3} [AddCommMonoid M] [AddCommMonoid M₁] [Semiring R] [Module R M] [Module R M₁] {f : M →ₗ[R] R} (hf : Function.Surjective ⇑f) (x : M₁) : (f.smulRight x).range = R ∙ x
• LinearMap.range_smulRight_apply 📋 Mathlib.Algebra.Module.LinearMap.DivisionRing
  {R : Type u_1} {M : Type u_2} {M₁ : Type u_3} [AddCommMonoid M] [AddCommMonoid M₁] [DivisionSemiring R] [Module R M] [Module R M₁] {f : M →ₗ[R] R} (hf : f ≠ 0) (x : M₁) : (f.smulRight x).range = R ∙ x
• ContinuousLinearMap.range_smulRight_apply 📋 Mathlib.Topology.Algebra.Module.LinearMap
  {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] {R : Type u_9} [DivisionSemiring R] [Module R M₁] [Module R M₂] [TopologicalSpace R] [ContinuousSMul R M₂] {f : M₁ →L[R] R} (hf : f ≠ 0) (x : M₂) : (↑(f.smulRight x)).range = R ∙ x
• Module.Basis.ofIsLocalizedModule_span 📋 Mathlib.RingTheory.Localization.Module
  {R : Type u_1} (Rₛ : Type u_2) [CommSemiring R] (S : Submonoid R) [CommSemiring Rₛ] [Algebra R Rₛ] [IsLocalization S Rₛ] {M : Type u_3} {Mₛ : Type u_4} [AddCommMonoid M] [Module R M] [AddCommMonoid Mₛ] [Module R Mₛ] [Module Rₛ Mₛ] [IsScalarTower R Rₛ Mₛ] (f : M →ₗ[R] Mₛ) [IsLocalizedModule S f] {ι : Type u_5} (b : Module.Basis ι R M) : Submodule.span R (Set.range ⇑(Module.Basis.ofIsLocalizedModule Rₛ S f b)) = f.range
• Module.Basis.localizationLocalization_span 📋 Mathlib.RingTheory.Localization.Module
  {R : Type u_1} (Rₛ : Type u_2) [CommSemiring R] (S : Submonoid R) [CommSemiring Rₛ] [Algebra R Rₛ] [IsLocalization S Rₛ] {A : Type u_3} [CommSemiring A] [Algebra R A] (Aₛ : Type u_4) [CommSemiring Aₛ] [Algebra A Aₛ] [Algebra Rₛ Aₛ] [Algebra R Aₛ] [IsScalarTower R Rₛ Aₛ] [IsScalarTower R A Aₛ] [IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ] {ι : Type u_5} (b : Module.Basis ι R A) : Submodule.span R (Set.range ⇑(Module.Basis.localizationLocalization Rₛ S Aₛ b)) = (↑(IsScalarTower.toAlgHom R A Aₛ)).range
• LinearMap.range_dualMap_dual_eq_span_singleton 📋 Mathlib.LinearAlgebra.Dual.Defs
  {R : Type u_1} {M₁ : Type u_2} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁] (f : Module.Dual R M₁) : (LinearMap.dualMap f).range = R ∙ f
• CharacterModule.intSpanEquivQuotAddOrderOf_symm_apply_coe 📋 Mathlib.Algebra.Module.CharacterModule
  {A : Type uA} [AddCommGroup A] (a : A) (a✝ : ℤ ⧸ Ideal.span {↑(addOrderOf a)}) : ↑((CharacterModule.intSpanEquivQuotAddOrderOf a).symm a✝) = ↑((LinearMap.toSpanSingleton ℤ A a).quotKerEquivRange (((LinearMap.toSpanSingleton ℤ A a).ker.quotEquivOfEq (Ideal.span {↑(addOrderOf a)}) ⋯).symm a✝))
• CharacterModule.intSpanEquivQuotAddOrderOf_apply 📋 Mathlib.Algebra.Module.CharacterModule
  {A : Type uA} [AddCommGroup A] (a : A) (a✝ : ↥(ℤ ∙ a)) : (CharacterModule.intSpanEquivQuotAddOrderOf a) a✝ = ((LinearMap.toSpanSingleton ℤ A a).ker.quotEquivOfEq (Ideal.span {↑(addOrderOf a)}) ⋯) ((LinearMap.toSpanSingleton ℤ A a).quotKerEquivRange.symm ((LinearEquiv.ofEq (ℤ ∙ a) (LinearMap.toSpanSingleton ℤ A a).range ⋯) a✝))
• Module.Relations.Solution.range_π 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] (solution : relations.Solution M) : solution.π.range = Submodule.span A (Set.range solution.var)
• Module.Relations.range_map 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] (relations : Module.Relations A) : relations.map.range = Submodule.span A (Set.range relations.relation)
• Matrix.isRepresentation.toEnd_exists_mem_ideal 📋 Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
  {ι : Type u_1} [Fintype ι] {M : Type u_2} [AddCommGroup M] (R : Type u_3) [CommRing R] [Module R M] (b : ι → M) [DecidableEq ι] (hb : Submodule.span R (Set.range b) = ⊤) (f : Module.End R M) (I : Ideal R) (hI : LinearMap.range f ≤ I • ⊤) : ∃ M_1, (Matrix.isRepresentation.toEnd R b hb) M_1 = f ∧ ∀ (i j : ι), ↑M_1 i j ∈ I
• LieModule.range_traceForm_le_span_weight 📋 Mathlib.Algebra.Lie.TraceForm
  (K : Type u_2) (L : Type u_3) (M : Type u_4) [LieRing L] [AddCommGroup M] [LieRingModule L M] [Field K] [LieAlgebra K L] [Module K M] [LieModule K L M] [FiniteDimensional K M] [LieRing.IsNilpotent L] [LieModule.LinearWeights K L M] [LieModule.IsTriangularizable K L M] : LinearMap.range (LieModule.traceForm K L M) ≤ Submodule.span K (Set.range (LieModule.Weight.toLinear K L M))
• LinearMap.IsPerfPair.restrictScalars_of_field 📋 Mathlib.LinearAlgebra.PerfectPairing.Restrict
  {K : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [Field K] [Field L] [Algebra K L] [AddCommGroup M] [AddCommGroup N] [Module L M] [Module L N] [Module K M] [Module K N] [IsScalarTower K L M] (p : M →ₗ[L] N →ₗ[L] L) [p.IsPerfPair] {M' : Type u_5} {N' : Type u_6} [AddCommGroup M'] [AddCommGroup N'] [Module K M'] [Module K N'] [IsScalarTower K L N] (i : M' →ₗ[K] M) (j : N' →ₗ[K] N) (hi : Function.Injective ⇑i) (hj : Function.Injective ⇑j) (hij : p.IsPerfectCompl (Submodule.span L ↑i.range) (Submodule.span L ↑j.range)) (hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap K L).range) : (i.restrictScalarsRange₂ j (Algebra.linearMap K L) ⋯ p hp).IsPerfPair
• 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 ↑i.range = ⊤) (hN : Submodule.span R ↑j.range = ⊤) (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
• RootPairing.root'_apply_apply_mem_of_mem_span 📋 Mathlib.LinearAlgebra.RootSystem.IsValuedIn
  {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_6) [CommRing S] [Algebra S R] [Module S N] [IsScalarTower S R N] [P.IsValuedIn S] {x : N} (hx : x ∈ Submodule.span S (Set.range ⇑P.coroot)) (i : ι) : (P.root' i) x ∈ (Algebra.linearMap S R).range
• Submodule.span_range_eq_top_of_injective_of_rank_le 📋 Mathlib.Algebra.Module.Lattice
  {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] {M N : Type u} [IsDomain R] [IsFractionRing R K] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module K N] [IsScalarTower R K N] [Module.Finite K N] {f : M →ₗ[R] N} (hf : Function.Injective ⇑f) (h : Module.rank K N ≤ Module.rank R M) : Submodule.span K ↑f.range = ⊤
• Module.Presentation.cokernel 📋 Mathlib.Algebra.Module.Presentation.Cokernel
  {A : Type u} [Ring A] {M₁ : Type v₁} {M₂ : Type v₂} [AddCommGroup M₁] [Module A M₁] [AddCommGroup M₂] [Module A M₂] (pres₂ : Module.Presentation A M₂) {f : M₁ →ₗ[A] M₂} {ι : Type w₁} {g₁ : ι → M₁} (data : pres₂.CokernelData f g₁) (hg₁ : Submodule.span A (Set.range g₁) = ⊤) : Module.Presentation A (M₂ ⧸ f.range)
• Module.Presentation.cokernelSolution.isPresentation 📋 Mathlib.Algebra.Module.Presentation.Cokernel
  {A : Type u} [Ring A] {M₁ : Type v₁} {M₂ : Type v₂} [AddCommGroup M₁] [Module A M₁] [AddCommGroup M₂] [Module A M₂] (pres₂ : Module.Presentation A M₂) {f : M₁ →ₗ[A] M₂} {ι : Type w₁} {g₁ : ι → M₁} (data : pres₂.CokernelData f g₁) (hg₁ : Submodule.span A (Set.range g₁) = ⊤) : (pres₂.cokernelSolution data).IsPresentation
• Module.Presentation.cokernelSolution.isPresentationCore 📋 Mathlib.Algebra.Module.Presentation.Cokernel
  {A : Type u} [Ring A] {M₁ : Type v₁} {M₂ : Type v₂} [AddCommGroup M₁] [Module A M₁] [AddCommGroup M₂] [Module A M₂] (pres₂ : Module.Presentation A M₂) {f : M₁ →ₗ[A] M₂} {ι : Type w₁} {g₁ : ι → M₁} (data : pres₂.CokernelData f g₁) (hg₁ : Submodule.span A (Set.range g₁) = ⊤) : (pres₂.cokernelSolution data).IsPresentationCore
• Module.Presentation.cokernel_G 📋 Mathlib.Algebra.Module.Presentation.Cokernel
  {A : Type u} [Ring A] {M₁ : Type v₁} {M₂ : Type v₂} [AddCommGroup M₁] [Module A M₁] [AddCommGroup M₂] [Module A M₂] (pres₂ : Module.Presentation A M₂) {f : M₁ →ₗ[A] M₂} {ι : Type w₁} {g₁ : ι → M₁} (data : pres₂.CokernelData f g₁) (hg₁ : Submodule.span A (Set.range g₁) = ⊤) : (pres₂.cokernel data hg₁).G = pres₂.G
• Module.Presentation.cokernel_R 📋 Mathlib.Algebra.Module.Presentation.Cokernel
  {A : Type u} [Ring A] {M₁ : Type v₁} {M₂ : Type v₂} [AddCommGroup M₁] [Module A M₁] [AddCommGroup M₂] [Module A M₂] (pres₂ : Module.Presentation A M₂) {f : M₁ →ₗ[A] M₂} {ι : Type w₁} {g₁ : ι → M₁} (data : pres₂.CokernelData f g₁) (hg₁ : Submodule.span A (Set.range g₁) = ⊤) : (pres₂.cokernel data hg₁).R = (pres₂.R ⊕ ι)
• Module.Presentation.cokernel_relation 📋 Mathlib.Algebra.Module.Presentation.Cokernel
  {A : Type u} [Ring A] {M₁ : Type v₁} {M₂ : Type v₂} [AddCommGroup M₁] [Module A M₁] [AddCommGroup M₂] [Module A M₂] (pres₂ : Module.Presentation A M₂) {f : M₁ →ₗ[A] M₂} {ι : Type w₁} {g₁ : ι → M₁} (data : pres₂.CokernelData f g₁) (hg₁ : Submodule.span A (Set.range g₁) = ⊤) (x✝ : pres₂.R ⊕ ι) : (pres₂.cokernel data hg₁).relation x✝ = match x✝ with | Sum.inl r => pres₂.relation r | Sum.inr i => data.lift i
• Module.Presentation.ofExact_var 📋 Mathlib.Algebra.Module.Presentation.Cokernel
  {A : Type u} [Ring A] {M₁ : Type v₁} {M₂ : Type v₂} {M₃ : Type v₃} [AddCommGroup M₁] [Module A M₁] [AddCommGroup M₂] [Module A M₂] [AddCommGroup M₃] [Module A M₃] {f : M₁ →ₗ[A] M₂} {g : M₂ →ₗ[A] M₃} (pres₂ : Module.Presentation A M₂) {ι : Type w₁} {g₁ : ι → M₁} (data : pres₂.CokernelData f g₁) (hfg : Function.Exact ⇑f ⇑g) (hg : Function.Surjective ⇑g) (hg₁ : Submodule.span A (Set.range g₁) = ⊤) (g✝ : (pres₂.cokernel data hg₁).G) : (pres₂.ofExact data hfg hg hg₁).var g✝ = g (pres₂.var g✝)
• Module.Presentation.cokernel_var 📋 Mathlib.Algebra.Module.Presentation.Cokernel
  {A : Type u} [Ring A] {M₁ : Type v₁} {M₂ : Type v₂} [AddCommGroup M₁] [Module A M₁] [AddCommGroup M₂] [Module A M₂] (pres₂ : Module.Presentation A M₂) {f : M₁ →ₗ[A] M₂} {ι : Type w₁} {g₁ : ι → M₁} (data : pres₂.CokernelData f g₁) (hg₁ : Submodule.span A (Set.range g₁) = ⊤) (g : (pres₂.cokernelRelations data).G) : (pres₂.cokernel data hg₁).var g = Submodule.Quotient.mk (pres₂.var g)
• ContinuousLinearEquiv.toSpanNonzeroSingleton_symm_apply 📋 Mathlib.Analysis.Normed.Module.Span
  (𝕜 : Type u_1) {E : Type u_2} [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (x : E) (h : x ≠ 0) (a✝ : ↥(𝕜 ∙ x)) : (ContinuousLinearEquiv.toSpanNonzeroSingleton 𝕜 x h).symm a✝ = (LinearEquiv.ofInjective (LinearMap.toSpanSingleton 𝕜 E x) ⋯).symm ((LinearEquiv.ofEq (𝕜 ∙ x) (LinearMap.toSpanSingleton 𝕜 E x).range ⋯) a✝)
• ZLattice.comap_span_top 📋 Mathlib.Algebra.Module.ZLattice.Basic
  (K : Type u_1) [NormedField K] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace K E] [NormedAddCommGroup F] [NormedSpace K F] (L : Submodule ℤ E) (hL : Submodule.span K ↑L = ⊤) {e : F →ₗ[K] E} (he : ↑L ⊆ ↑e.range) : Submodule.span K ↑(ZLattice.comap K L e) = ⊤
• IsIntegralClosure.range_le_span_dualBasis 📋 Mathlib.RingTheory.DedekindDomain.IntegralClosure
  {A : Type u_1} {K : Type u_2} [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] {L : Type u_3} [Field L] (C : Type u_4) [CommRing C] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [Algebra C L] [IsIntegralClosure C A L] [Algebra A C] [IsScalarTower A C L] [FiniteDimensional K L] [Algebra.IsSeparable K L] {ι : Type u_5} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι K L) (hb_int : ∀ (i : ι), IsIntegral A (b i)) [IsIntegrallyClosed A] : (↑A (Algebra.linearMap C L)).range ≤ Submodule.span A (Set.range ⇑((Algebra.traceForm K L).dualBasis ⋯ b))
• PiTensorProduct.map_range_eq_span_tprod 📋 Mathlib.LinearAlgebra.PiTensorProduct
  {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ι → Type u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {t : ι → Type u_11} [(i : ι) → AddCommMonoid (t i)] [(i : ι) → Module R (t i)] (f : (i : ι) → s i →ₗ[R] t i) : (PiTensorProduct.map f).range = Submodule.span R {t_1 | ∃ m, (⨂ₜ[R] (i : ι), (f i) (m i)) = t_1}
• range_mfderiv_coe_sphere 📋 Mathlib.Geometry.Manifold.Instances.Sphere
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] (v : ↑(Metric.sphere 0 1)) : (↑(mfderiv (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) (modelWithCornersSelf ℝ E) Subtype.val v)).range = (ℝ ∙ ↑v)ᗮ
• RootPairing.GeckConstruction.span_range_h_le_range_diagonal 📋 Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
  {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.IsCrystallographic] {b : P.Base} [DecidableEq ι] : Submodule.span R (Set.range RootPairing.GeckConstruction.h) ≤ (Matrix.diagonalLinearMap (↥b.support ⊕ ι) R R).range

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 abad10c