Loogle!

Result

Found 40 declarations mentioning Basis.map.

• Basis.map 📋 Mathlib.LinearAlgebra.Basis.Defs
  {ι : Type u_1} {R : Type u_3} {M : Type u_6} {M' : Type u_7} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (b : Basis ι R M) (f : M ≃ₗ[R] M') : Basis ι R M'
• Basis.map_equiv 📋 Mathlib.LinearAlgebra.Basis.Defs
  {ι' : Type u_2} {M' : Type u_7} [AddCommMonoid M'] {ι : Type u_10} {R : Type u_11} {M : Type u_12} [Semiring R] [AddCommMonoid M] [Module R M] [Module R M'] (b : Basis ι R M) (b' : Basis ι' R M') (e : ι ≃ ι') : b.map (b.equiv b' e) = b'.reindex e.symm
• Basis.map_apply 📋 Mathlib.LinearAlgebra.Basis.Defs
  {ι : Type u_1} {R : Type u_3} {M : Type u_6} {M' : Type u_7} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (b : Basis ι R M) (f : M ≃ₗ[R] M') (i : ι) : (b.map f) i = f (b i)
• Basis.coe_map 📋 Mathlib.LinearAlgebra.Basis.Defs
  {ι : Type u_1} {R : Type u_3} {M : Type u_6} {M' : Type u_7} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (b : Basis ι R M) (f : M ≃ₗ[R] M') : ⇑(b.map f) = ⇑f ∘ ⇑b
• Basis.map_repr 📋 Mathlib.LinearAlgebra.Basis.Defs
  {ι : Type u_1} {R : Type u_3} {M : Type u_6} {M' : Type u_7} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (b : Basis ι R M) (f : M ≃ₗ[R] M') : (b.map f).repr = f.symm ≪≫ₗ b.repr
• Basis.map_equivFun 📋 Mathlib.LinearAlgebra.Basis.Defs
  {ι : Type u_1} {R : Type u_3} {M : Type u_6} {M' : Type u_7} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] [Finite ι] (b : Basis ι R M) (f : M ≃ₗ[R] M') : (b.map f).equivFun = f.symm ≪≫ₗ b.equivFun
• Basis.tensorProduct.eq_1 📋 Mathlib.LinearAlgebra.TensorProduct.Basis
  {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} {ι : Type u_5} {κ : Type u_6} [CommSemiring R] [Semiring S] [Algebra R S] [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower R S M] [AddCommMonoid N] [Module R N] (b : Basis ι S M) (c : Basis κ R N) : b.tensorProduct c = Finsupp.basisSingleOne.map (TensorProduct.AlgebraTensorModule.congr b.repr c.repr ≪≫ₗ (finsuppTensorFinsupp R S S R ι κ ≪≫ₗ Finsupp.lcongr (Equiv.refl (ι × κ)) (TensorProduct.AlgebraTensorModule.rid R S S))).symm
• Basis.addSubgroupOfClosure.eq_1 📋 Mathlib.LinearAlgebra.Basis.Submodule
  {M : Type u_7} {R : Type u_8} [Ring R] [Nontrivial R] [NoZeroSMulDivisors ℤ R] [AddCommGroup M] [Module R M] (A : AddSubgroup M) {ι : Type u_9} (b : Basis ι R M) (h : A = AddSubgroup.closure (Set.range ⇑b)) : Basis.addSubgroupOfClosure A b h = (Basis.restrictScalars ℤ b).map (LinearEquiv.ofEq (Submodule.span ℤ (Set.range ⇑b)) (AddSubgroup.toIntSubmodule A) ⋯)
• Basis.matrix.eq_1 📋 Mathlib.LinearAlgebra.Matrix.StdBasis
  {ι : Type u_1} {R : Type u_2} {M : Type u_3} (m : Type u_4) (n : Type u_5) [Fintype m] [Fintype n] [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) : Basis.matrix m n b = ((Pi.basis fun x => Pi.basis fun x => b).reindex ((Equiv.sigmaEquivProd m ((_ : n) × ι)).trans ((Equiv.refl m).prodCongr (Equiv.sigmaEquivProd n ι)))).map (Matrix.ofLinearEquiv R)
• Matrix.stdBasis.eq_1 📋 Mathlib.LinearAlgebra.Matrix.StdBasis
  (R : Type u_1) (m : Type u_2) (n : Type u_3) [Fintype m] [Finite n] [Semiring R] : Matrix.stdBasis R m n = ((Pi.basis fun x => Pi.basisFun R n).reindex (Equiv.sigmaEquivProd m n)).map (Matrix.ofLinearEquiv R)
• Basis.smul_eq_map 📋 Mathlib.LinearAlgebra.Basis.SMul
  {ι : Type u_1} {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (g : M ≃ₗ[R] M) (b : Basis ι R M) : g • b = b.map g
• Basis.linearMap.eq_1 📋 Mathlib.LinearAlgebra.Matrix.ToLin
  {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} {ι₁ : Type u_6} {ι₂ : Type u_7} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] [Fintype ι₁] [Fintype ι₂] [DecidableEq ι₁] (b₁ : Basis ι₁ R M₁) (b₂ : Basis ι₂ R M₂) : b₁.linearMap b₂ = (Matrix.stdBasis R ι₂ ι₁).map (LinearMap.toMatrix b₁ b₂).symm
• Basis.dualBasis.eq_1 📋 Mathlib.LinearAlgebra.Dual.Basis
  {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Basis ι R M) [Finite ι] : b.dualBasis = b.map b.toDualEquiv
• Basis.map.eq_1 📋 Mathlib.LinearAlgebra.Matrix.Basis
  {ι : Type u_1} {R : Type u_3} {M : Type u_6} {M' : Type u_7} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (b : Basis ι R M) (f : M ≃ₗ[R] M') : b.map f = { repr := f.symm ≪≫ₗ b.repr }
• Basis.toMatrix_map 📋 Mathlib.LinearAlgebra.Matrix.Basis
  {ι : Type u_1} {R : Type u_5} {M : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Type u_9} [AddCommMonoid N] [Module R N] (b : Basis ι R M) (f : M ≃ₗ[R] N) (v : ι → N) : (b.map f).toMatrix v = b.toMatrix (⇑f.symm ∘ v)
• Basis.det_map' 📋 Mathlib.LinearAlgebra.Determinant
  {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {M' : Type u_3} [AddCommGroup M'] [Module R M'] {ι : Type u_4} [DecidableEq ι] [Fintype ι] (b : Basis ι R M) (f : M ≃ₗ[R] M') : (b.map f).det = b.det.compLinearMap ↑f.symm
• Basis.det_map 📋 Mathlib.LinearAlgebra.Determinant
  {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {M' : Type u_3} [AddCommGroup M'] [Module R M'] {ι : Type u_4} [DecidableEq ι] [Fintype ι] (b : Basis ι R M) (f : M ≃ₗ[R] M') (v : ι → M') : (b.map f).det v = b.det (⇑f.symm ∘ v)
• LinearMap.BilinForm.dualBasis.eq_1 📋 Mathlib.LinearAlgebra.BilinearForm.Properties
  {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] {ι : Type u_9} [DecidableEq ι] [Finite ι] (B : LinearMap.BilinForm K V) (hB : B.Nondegenerate) (b : Basis ι K V) : B.dualBasis hB b = b.dualBasis.map (B.toDual hB).symm
• PowerBasis.map_basis 📋 Mathlib.RingTheory.PowerBasis
  {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {S' : Type u_7} [CommRing S'] [Algebra R S'] (pb : PowerBasis R S) (e : S ≃ₐ[R] S') : (pb.map e).basis = pb.basis.map e.toLinearEquiv
• IntermediateField.powerBasisAux.eq_1 📋 Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
  {K : Type u} [Field K] {L : Type u_3} [Field L] [Algebra K L] {x : L} (hx : IsIntegral K x) : IntermediateField.powerBasisAux hx = ((AdjoinRoot.powerBasis ⋯).basis.map (IntermediateField.adjoinRootEquivAdjoin K hx).toLinearEquiv).reindex (finCongr ⋯)
• Orthonormal.mapLinearIsometryEquiv 📋 Mathlib.Analysis.InnerProductSpace.Orthonormal
  {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {E' : Type u_7} [SeminormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] {v : Basis ι 𝕜 E} (hv : Orthonormal 𝕜 ⇑v) (f : E ≃ₗᵢ[𝕜] E') : Orthonormal 𝕜 ⇑(v.map f.toLinearEquiv)
• Orthonormal.map_equiv 📋 Mathlib.Analysis.InnerProductSpace.Orthonormal
  {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {ι' : Type u_5} {E' : Type u_7} [SeminormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] {v : Basis ι 𝕜 E} (hv : Orthonormal 𝕜 ⇑v) {v' : Basis ι' 𝕜 E'} (hv' : Orthonormal 𝕜 ⇑v') (e : ι ≃ ι') : v.map (hv.equiv hv' e).toLinearEquiv = v'.reindex e.symm
• PiLp.basisFun_map 📋 Mathlib.Analysis.Normed.Lp.PiLp
  (p : ENNReal) (𝕜 : Type u_1) (ι : Type u_2) [Finite ι] [Ring 𝕜] : (PiLp.basisFun p 𝕜 ι).map (WithLp.linearEquiv p 𝕜 (ι → 𝕜)) = Pi.basisFun 𝕜 ι
• PiLp.basisFun_eq_pi_basisFun 📋 Mathlib.Analysis.Normed.Lp.PiLp
  (p : ENNReal) (𝕜 : Type u_1) (ι : Type u_2) [Finite ι] [Ring 𝕜] : PiLp.basisFun p 𝕜 ι = (Pi.basisFun 𝕜 ι).map (WithLp.linearEquiv p 𝕜 (ι → 𝕜)).symm
• OrthonormalBasis.toBasis_map 📋 Mathlib.Analysis.InnerProductSpace.PiL2
  {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {G : Type u_7} [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] (b : OrthonormalBasis ι 𝕜 E) (L : E ≃ₗᵢ[𝕜] G) : (b.map L).toBasis = b.toBasis.map L.toLinearEquiv
• Pi.orthonormalBasis.toBasis 📋 Mathlib.Analysis.InnerProductSpace.PiL2
  {η : Type u_7} [Fintype η] {ι : η → Type u_8} [(i : η) → Fintype (ι i)] {𝕜 : Type u_9} [RCLike 𝕜] {E : η → Type u_10} [(i : η) → NormedAddCommGroup (E i)] [(i : η) → InnerProductSpace 𝕜 (E i)] (B : (i : η) → OrthonormalBasis (ι i) 𝕜 (E i)) : (Pi.orthonormalBasis B).toBasis = (Pi.basis fun i => (B i).toBasis).map (WithLp.linearEquiv 2 𝕜 ((j : η) → E j)).symm
• Basis.parallelepiped_map 📋 Mathlib.MeasureTheory.Measure.Haar.OfBasis
  {ι : Type u_1} {E : Type u_3} {F : Type u_4} [Fintype ι] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ F] (b : Basis ι ℝ E) (e : E ≃ₗ[ℝ] F) : (b.map e).parallelepiped = TopologicalSpace.PositiveCompacts.map ⇑e ⋯ ⋯ b.parallelepiped
• Basis.map_addHaar 📋 Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
  {ι : Type u_1} {E : Type u_2} {F : Type u_3} [Fintype ι] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ F] [MeasurableSpace E] [MeasurableSpace F] [BorelSpace E] [BorelSpace F] [SecondCountableTopology F] [SigmaCompactSpace F] (b : Basis ι ℝ E) (f : E ≃L[ℝ] F) : MeasureTheory.Measure.map (⇑f) b.addHaar = (b.map f.toLinearEquiv).addHaar
• ZSpan.map_fundamentalDomain 📋 Mathlib.Algebra.Module.ZLattice.Basic
  {E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) [LinearOrder K] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace K F] (f : E ≃ₗ[K] F) : ⇑f '' ZSpan.fundamentalDomain b = ZSpan.fundamentalDomain (b.map f)
• ZSpan.map 📋 Mathlib.Algebra.Module.ZLattice.Basic
  {E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) {F : Type u_4} [AddCommGroup F] [Module K F] (f : E ≃ₗ[K] F) : Submodule.map (LinearEquiv.restrictScalars ℤ f) (Submodule.span ℤ (Set.range ⇑b)) = Submodule.span ℤ (Set.range ⇑(b.map f))
• Basis.ofZLatticeBasis_comap 📋 Mathlib.Algebra.Module.ZLattice.Basic
  (K : Type u_1) [NormedField K] [LinearOrder K] [IsStrictOrderedRing K] [HasSolidNorm K] [FloorRing K] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace K E] [FiniteDimensional K E] [ProperSpace E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace K F] [FiniteDimensional K F] [ProperSpace F] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice K L] (e : F ≃L[K] E) {ι : Type u_4} (b : Basis ι ℤ ↥L) : Basis.ofZLatticeBasis K (ZLattice.comap K L ↑e.toLinearEquiv) (Basis.ofZLatticeComap K L e.toLinearEquiv b) = (Basis.ofZLatticeBasis K L b).map e.symm.toLinearEquiv
• Basis.ofZLatticeComap.eq_1 📋 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) (e : F ≃ₗ[K] E) {ι : Type u_4} (b : Basis ι ℤ ↥L) : Basis.ofZLatticeComap K L e b = b.map (ZLattice.comap_equiv K L e)
• Basis.orientation_map 📋 Mathlib.LinearAlgebra.Orientation
  {R : Type u_1} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (e : Basis ι R M) (f : M ≃ₗ[R] N) : (e.map f).orientation = (Orientation.map ι f) e.orientation
• Basis.orientation_comp_linearEquiv_eq_iff_det_pos 📋 Mathlib.LinearAlgebra.Orientation
  {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_3} [Fintype ι] [DecidableEq ι] (e : Basis ι R M) (f : M ≃ₗ[R] M) : (e.map f).orientation = e.orientation ↔ 0 < LinearMap.det ↑f
• Basis.orientation_comp_linearEquiv_eq_neg_iff_det_neg 📋 Mathlib.LinearAlgebra.Orientation
  {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_3} [Fintype ι] [DecidableEq ι] (e : Basis ι R M) (f : M ≃ₗ[R] M) : (e.map f).orientation = -e.orientation ↔ LinearMap.det ↑f < 0
• Algebra.SubmersivePresentation.basisDeriv.eq_1 📋 Mathlib.RingTheory.Smooth.StandardSmooth
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.SubmersivePresentation R S) : P.basisDeriv = (Pi.basisFun S P.rels).map P.aevalDifferentialEquiv
• Algebra.SubmersivePresentation.basisCotangent.eq_1 📋 Mathlib.RingTheory.Smooth.StandardSmoothCotangent
  {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.SubmersivePresentation R S) : P.basisCotangent = P.basisDeriv.map P.cotangentEquiv.symm
• Ideal.basisSpanSingleton.eq_1 📋 Mathlib.RingTheory.Ideal.Basis
  {ι : Type u_1} {R : Type u_2} {S : Type u_3} [CommSemiring R] [CommRing S] [IsDomain S] [Algebra R S] (b : Basis ι R S) {x : S} (hx : x ≠ 0) : Ideal.basisSpanSingleton b hx = b.map (((LinearEquiv.ofInjective (LinearMap.mulLeft R x) ⋯).trans (LinearEquiv.ofEq (LinearMap.range (LinearMap.mulLeft R x)) (Submodule.restrictScalars R (Ideal.span {x})) ⋯)).trans (LinearEquiv.restrictScalars R (Submodule.restrictScalarsEquiv R S S (Ideal.span {x}))))
• NumberField.mixedEmbedding.euclidean.stdOrthonormalBasis_map_eq 📋 Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
  (K : Type u_1) [Field K] [NumberField K] : (NumberField.mixedEmbedding.euclidean.stdOrthonormalBasis K).toBasis.map (NumberField.mixedEmbedding.euclidean.toMixed K).toLinearEquiv = NumberField.mixedEmbedding.stdBasis K
• NumberField.Units.basisUnitLattice.eq_1 📋 Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
  (K : Type u_1) [Field K] [NumberField K] : NumberField.Units.basisUnitLattice K = (NumberField.Units.basisModTorsion K).map (NumberField.Units.logEmbeddingEquiv K)

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