Loogle!

Result

Found 247 declarations mentioning Module.Basis.repr. Of these, only the first 200 are shown.

• Module.Basis.repr 📋 Mathlib.LinearAlgebra.Basis.Defs
  {ι : Type u_1} {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (self : Module.Basis ι R M) : M ≃ₗ[R] ι →₀ R
• Module.Basis.repr_injective 📋 Mathlib.LinearAlgebra.Basis.Defs
  {ι : Type u_1} {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] : Function.Injective Module.Basis.repr
• Module.Basis.coe_repr_symm 📋 Mathlib.LinearAlgebra.Basis.Defs
  {ι : Type u_1} {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) : ↑b.repr.symm = Finsupp.linearCombination R ⇑b
• Module.Basis.repr_self 📋 Mathlib.LinearAlgebra.Basis.Defs
  {ι : Type u_1} {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) (i : ι) : b.repr (b i) = fun₀ | i => 1
• Module.Basis.map_repr 📋 Mathlib.LinearAlgebra.Basis.Defs
  {ι : Type u_1} {R : Type u_3} {M : Type u_4} {M' : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (b : Module.Basis ι R M) (f : M ≃ₗ[R] M') : (b.map f).repr = f.symm ≪≫ₗ b.repr
• Module.Basis.apply_eq_iff 📋 Mathlib.LinearAlgebra.Basis.Defs
  {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] {b : Module.Basis ι R M} {x : M} {i : ι} : b i = x ↔ b.repr x = fun₀ | i => 1
• Module.Basis.coe_sumCoords 📋 Mathlib.LinearAlgebra.Basis.Defs
  {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) : ⇑b.sumCoords = fun m => (b.repr m).sum fun x => id
• Module.Basis.repr_self_apply 📋 Mathlib.LinearAlgebra.Basis.Defs
  {ι : Type u_1} {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) (i j : ι) [Decidable (i = j)] : (b.repr (b i)) j = if i = j then 1 else 0
• Module.Basis.coord_apply 📋 Mathlib.LinearAlgebra.Basis.Defs
  {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) (i : ι) (x : M) : (b.coord i) x = (b.repr x) i
• Module.Basis.sum_repr 📋 Mathlib.LinearAlgebra.Basis.Defs
  {ι : Type u_1} {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [Fintype ι] (b : Module.Basis ι R M) (u : M) : ∑ i, (b.repr u) i • b i = u
• Module.Basis.repr_sum_self 📋 Mathlib.LinearAlgebra.Basis.Defs
  {ι : Type u_1} {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [Fintype ι] (b : Module.Basis ι R M) (c : ι → R) : ⇑(b.repr (∑ i, c i • b i)) = c
• Module.Basis.repr_eq_iff 📋 Mathlib.LinearAlgebra.Basis.Defs
  {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] {b : Module.Basis ι R M} {f : M →ₗ[R] ι →₀ R} : ↑b.repr = f ↔ ∀ (i : ι), f (b i) = fun₀ | i => 1
• Module.Basis.repr_symm_single_one 📋 Mathlib.LinearAlgebra.Basis.Defs
  {ι : Type u_1} {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) (i : ι) : (b.repr.symm fun₀ | i => 1) = b i
• Module.Basis.linearCombination_repr 📋 Mathlib.LinearAlgebra.Basis.Defs
  {ι : Type u_1} {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) (x : M) : (Finsupp.linearCombination R ⇑b) (b.repr x) = x
• Module.Basis.repr_symm_single 📋 Mathlib.LinearAlgebra.Basis.Defs
  {ι : Type u_1} {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) (i : ι) (c : R) : (b.repr.symm fun₀ | i => c) = c • b i
• Module.Basis.repr_linearCombination 📋 Mathlib.LinearAlgebra.Basis.Defs
  {ι : Type u_1} {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) (v : ι →₀ R) : b.repr ((Finsupp.linearCombination R ⇑b) v) = v
• Module.Basis.coord_repr_symm 📋 Mathlib.LinearAlgebra.Basis.Defs
  {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) (i : ι) (f : ι →₀ R) : (b.coord i) (b.repr.symm f) = f i
• Module.Basis.repr_eq_iff' 📋 Mathlib.LinearAlgebra.Basis.Defs
  {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] {b : Module.Basis ι R M} {f : M ≃ₗ[R] ι →₀ R} : b.repr = f ↔ ∀ (i : ι), f (b i) = fun₀ | i => 1
• Module.Basis.equivFun_apply 📋 Mathlib.LinearAlgebra.Basis.Defs
  {ι : Type u_1} {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [Finite ι] (b : Module.Basis ι R M) (u : M) : b.equivFun u = ⇑(b.repr u)
• Module.Basis.repr_symm_apply 📋 Mathlib.LinearAlgebra.Basis.Defs
  {ι : Type u_1} {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) (v : ι →₀ R) : b.repr.symm v = (Finsupp.linearCombination R ⇑b) v
• Module.Basis.repr_reindex 📋 Mathlib.LinearAlgebra.Basis.Defs
  {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) (x : M) (e : ι ≃ ι') : (b.reindex e).repr x = Finsupp.equivMapDomain e (b.repr x)
• Module.Basis.repr_apply_eq 📋 Mathlib.LinearAlgebra.Basis.Defs
  {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) (f : M → ι → R) (hadd : ∀ (x y : M), f (x + y) = f x + f y) (hsmul : ∀ (c : R) (x : M), f (c • x) = c • f x) (f_eq : ∀ (i : ι), f (b i) = ⇑fun₀ | i => 1) (x : M) (i : ι) : (b.repr x) i = f x i
• Module.Basis.ofEquivFun_repr_apply 📋 Mathlib.LinearAlgebra.Basis.Defs
  {ι : Type u_1} {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [Finite ι] (e : M ≃ₗ[R] ι → R) (x : M) (i : ι) : ((Module.Basis.ofEquivFun e).repr x) i = e x i
• Module.Basis.ext_elem 📋 Mathlib.LinearAlgebra.Basis.Defs
  {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) {x y : M} : (∀ (i : ι), (b.repr x) i = (b.repr y) i) → x = y
• Module.Basis.ext_elem_iff 📋 Mathlib.LinearAlgebra.Basis.Defs
  {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) {x y : M} : x = y ↔ ∀ (i : ι), (b.repr x) i = (b.repr y) i
• Module.Basis.eq_ofRepr_eq_repr 📋 Mathlib.LinearAlgebra.Basis.Defs
  {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] {b₁ b₂ : Module.Basis ι R M} (h : ∀ (x : M) (i : ι), (b₁.repr x) i = (b₂.repr x) i) : b₁ = b₂
• Module.Basis.repr_reindex_apply 📋 Mathlib.LinearAlgebra.Basis.Defs
  {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) (x : M) (e : ι ≃ ι') (i' : ι') : ((b.reindex e).repr x) i' = (b.repr x) (e.symm i')
• Module.Basis.reindexRange_repr_self 📋 Mathlib.LinearAlgebra.Basis.Defs
  {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) (i : ι) : b.reindexRange.repr (b i) = fun₀ | ⟨b i, ⋯⟩ => 1
• Module.Basis.constr_def 📋 Mathlib.LinearAlgebra.Basis.Defs
  {M' : Type u_5} [AddCommMonoid M'] {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) [Module R M'] (S : Type u_10) [Semiring S] [Module S M'] [SMulCommClass R S M'] (f : ι → M') : (b.constr S) f = Finsupp.linearCombination R id ∘ₗ Finsupp.lmapDomain R R f ∘ₗ ↑b.repr
• Module.Basis.constr_apply 📋 Mathlib.LinearAlgebra.Basis.Defs
  {M' : Type u_5} [AddCommMonoid M'] {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) [Module R M'] (S : Type u_10) [Semiring S] [Module S M'] [SMulCommClass R S M'] (f : ι → M') (x : M) : ((b.constr S) f) x = (b.repr x).sum fun b a => a • f b
• Module.Basis.reindexRange_repr' 📋 Mathlib.LinearAlgebra.Basis.Defs
  {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) (x : M) {bi : M} {i : ι} (h : b i = bi) : (b.reindexRange.repr x) ⟨bi, ⋯⟩ = (b.repr x) i
• Module.Basis.reindexFinsetRange_repr_self 📋 Mathlib.LinearAlgebra.Basis.Defs
  {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) [Fintype ι] [DecidableEq M] (i : ι) : b.reindexFinsetRange.repr (b i) = fun₀ | ⟨b i, ⋯⟩ => 1
• Module.Basis.sum_repr_mul_repr 📋 Mathlib.LinearAlgebra.Basis.Defs
  {ι : Type u_7} {R : Type u_11} {M : Type u_12} [CommSemiring R] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) {ι' : Type u_14} [Fintype ι'] (b' : Module.Basis ι' R M) (x : M) (i : ι) : ∑ j, (b.repr (b' j)) i * (b'.repr x) j = (b.repr x) i
• Module.Basis.reindexRange_repr 📋 Mathlib.LinearAlgebra.Basis.Defs
  {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) (x : M) (i : ι) (h : b i ∈ Set.range ⇑b := ⋯) : (b.reindexRange.repr x) ⟨b i, h⟩ = (b.repr x) i
• Module.Basis.mapCoeffs_repr 📋 Mathlib.LinearAlgebra.Basis.Defs
  {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) {R' : Type u_10} [Semiring R'] [Module R' M] (f : R ≃+* R') (h : ∀ (c : R) (x : M), f c • x = c • x) : (b.mapCoeffs f h).repr = LinearEquiv.restrictScalars R' b.repr ≪≫ₗ Finsupp.mapRange.linearEquiv (Module.compHom.toLinearEquiv f.symm).symm
• Module.Basis.reindexFinsetRange_repr 📋 Mathlib.LinearAlgebra.Basis.Defs
  {ι : Type u_7} {R : Type u_8} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) [Fintype ι] [DecidableEq M] (x : M) (i : ι) (h : b i ∈ Finset.image (⇑b) Finset.univ := ⋯) : (b.reindexFinsetRange.repr x) ⟨b i, h⟩ = (b.repr x) i
• Module.Basis.repr_range 📋 Mathlib.LinearAlgebra.Basis.Basic
  {ι : Type u_1} {R : Type u_2} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) : (↑b.repr).range = Finsupp.supported R R Set.univ
• Module.Basis.singleton_repr 📋 Mathlib.LinearAlgebra.Basis.Basic
  (ι : Type u_6) (R : Type u_7) [Unique ι] [Semiring R] (x : R) (i : ι) : ((Module.Basis.singleton ι R).repr x) i = x
• Module.Basis.mem_span_repr_support 📋 Mathlib.LinearAlgebra.Basis.Basic
  {ι : Type u_1} {R : Type u_2} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) (m : M) : m ∈ Submodule.span R (⇑b '' ↑(b.repr m).support)
• Module.Basis.repr_support_subset_of_mem_span 📋 Mathlib.LinearAlgebra.Basis.Basic
  {ι : Type u_1} {R : Type u_2} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) (s : Set ι) {m : M} (hm : m ∈ Submodule.span R (⇑b '' s)) : ↑(b.repr m).support ⊆ s
• Module.Basis.mem_span_image 📋 Mathlib.LinearAlgebra.Basis.Basic
  {ι : Type u_1} {R : Type u_2} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) {m : M} {s : Set ι} : m ∈ Submodule.span R (⇑b '' s) ↔ ↑(b.repr m).support ⊆ s
• Module.Basis.mk_repr 📋 Mathlib.LinearAlgebra.Basis.Basic
  {ι : Type u_1} {R : Type u_2} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {v : ι → M} {x : M} (hli : LinearIndependent R v) (hsp : ⊤ ≤ Submodule.span R (Set.range v)) : (Module.Basis.mk hli hsp).repr x = hli.repr ⟨x, ⋯⟩
• Module.Basis.span_repr_eq_single 📋 Mathlib.LinearAlgebra.Basis.Basic
  {ι : Type u_1} {R : Type u_2} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {v : ι → M} (hli : LinearIndependent R v) (i : ι) (hi : v i ∈ Submodule.span R (Set.range v) := ⋯) : (Module.Basis.span hli).repr ⟨v i, hi⟩ = fun₀ | i => 1
• Module.Basis.mem_span_iff_repr_mem 📋 Mathlib.LinearAlgebra.Basis.Submodule
  {ι : Type u_1} (R : Type u_2) {M : Type u_3} {S : Type u_4} [CommRing R] [IsDomain R] [Ring S] [Nontrivial S] [AddCommGroup M] [Algebra R S] [Module S M] [Module R M] [IsScalarTower R S M] [Module.IsTorsionFree R S] (b : Module.Basis ι S M) (m : M) : m ∈ Submodule.span R (Set.range ⇑b) ↔ ∀ (i : ι), (b.repr m) i ∈ Set.range ⇑(algebraMap R S)
• Module.Basis.restrictScalars_repr_apply 📋 Mathlib.LinearAlgebra.Basis.Submodule
  {ι : Type u_1} (R : Type u_2) {M : Type u_3} {S : Type u_4} [CommRing R] [IsDomain R] [Ring S] [Nontrivial S] [AddCommGroup M] [Algebra R S] [Module S M] [Module R M] [IsScalarTower R S M] [Module.IsTorsionFree R S] (b : Module.Basis ι S M) (m : ↥(Submodule.span R (Set.range ⇑b))) (i : ι) : (algebraMap R S) (((Module.Basis.restrictScalars R b).repr m) i) = (b.repr ↑m) i
• Module.Basis.addSubgroupOfClosure_repr_apply 📋 Mathlib.LinearAlgebra.Basis.Submodule
  {M : Type u_4} {R : Type u_5} [Ring R] [Nontrivial R] [IsAddTorsionFree R] [AddCommGroup M] [Module R M] (A : AddSubgroup M) {ι : Type u_6} (b : Module.Basis ι R M) (h : A = AddSubgroup.closure (Set.range ⇑b)) (x : ↥A) (i : ι) : ↑(((Module.Basis.addSubgroupOfClosure A b h).repr x) i) = (b.repr ↑x) i
• union_support_maximal_linearIndependent_eq_range_basis 📋 Mathlib.LinearAlgebra.Basis.Cardinality
  {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Nontrivial R] [Module R M] {ι : Type w} (b : Module.Basis ι R M) {κ : Type w'} (v : κ → M) (ind : LinearIndependent R v) (m : ind.Maximal) : ⋃ k, ↑(b.repr (v k)).support = Set.univ
• Module.Basis.repr_algebraMap 📋 Mathlib.LinearAlgebra.FreeModule.Basic
  {R : Type u} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {ι : Type u_3} {B : Module.Basis ι R S} {i : ι} (hBi : B i = 1) (r : R) : B.repr ((algebraMap R S) r) = fun₀ | i => r
• Finsupp.basisSingleOne_repr 📋 Mathlib.LinearAlgebra.Finsupp.VectorSpace
  {R : Type u_1} {ι : Type u_3} [Semiring R] : Finsupp.basisSingleOne.repr = LinearEquiv.refl R (ι →₀ R)
• Finsupp.basis_repr 📋 Mathlib.LinearAlgebra.Finsupp.VectorSpace
  {R : Type u_1} {M : Type u_2} {ι : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {φ : ι → Type u_4} (b : (i : ι) → Module.Basis (φ i) R M) (g : ι →₀ M) (ix : (i : ι) × φ i) : ((Finsupp.basis b).repr g) ix = ((b ix.fst).repr (g ix.fst)) ix.snd
• Module.Basis.repr_smul' 📋 Mathlib.LinearAlgebra.Finsupp.VectorSpace
  {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {ι : Type u_3} (B : Module.Basis ι R S) (i : ι) (r : R) (s : S) : (B.repr ((algebraMap R S) r * s)) i = r * (B.repr s) i
• Pi.basisFun_repr 📋 Mathlib.LinearAlgebra.StdBasis
  (R : Type u_2) (η : Type u_4) [Semiring R] [Finite η] (x : η → R) (i : η) : ((Pi.basisFun R η).repr x) i = x i
• Pi.basis_repr_single 📋 Mathlib.LinearAlgebra.StdBasis
  {R : Type u_2} {η : Type u_4} {ιs : η → Type u_5} {Ms : η → Type u_6} [Semiring R] [(i : η) → AddCommMonoid (Ms i)] [(i : η) → Module R (Ms i)] [Fintype η] [DecidableEq η] (s : (j : η) → Module.Basis (ιs j) R (Ms j)) (j : η) (i : ιs j) : (Pi.basis s).repr (Pi.single j ((s j) i)) = fun₀ | ⟨j, i⟩ => 1
• Pi.basis_repr 📋 Mathlib.LinearAlgebra.StdBasis
  {R : Type u_2} {η : Type u_4} {ιs : η → Type u_5} {Ms : η → Type u_6} [Semiring R] [(i : η) → AddCommMonoid (Ms i)] [(i : η) → Module R (Ms i)] [Fintype η] (s : (j : η) → Module.Basis (ιs j) R (Ms j)) (x : (j : η) → Ms j) (ji : (j : η) × ιs j) : ((Pi.basis s).repr x) ji = ((s ji.fst).repr (x ji.fst)) ji.snd
• Module.Basis.algebraMapCoeffs_repr_apply_apply 📋 Mathlib.RingTheory.AlgebraTower
  {R : Type u_1} (A : Type u_3) {ι : Type u_5} {M : Type u_6} [CommSemiring R] [Semiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] [IsScalarTower R A M] (b : Module.Basis ι R M) (h : Function.Bijective ⇑(algebraMap R A)) (x : M) (a✝ : ι) : ((Module.Basis.algebraMapCoeffs A b h).repr x) a✝ = (algebraMap R A) ((b.repr x) a✝)
• Module.Basis.algebraMapCoeffs_repr 📋 Mathlib.RingTheory.AlgebraTower
  {R : Type u_1} (A : Type u_3) {ι : Type u_5} {M : Type u_6} [CommSemiring R] [Semiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] [IsScalarTower R A M] (b : Module.Basis ι R M) (h : Function.Bijective ⇑(algebraMap R A)) (m : M) : (Module.Basis.algebraMapCoeffs A b h).repr m = Finsupp.mapRange ⇑(algebraMap R A) ⋯ (b.repr m)
• Module.Basis.smulTower'_repr_mk 📋 Mathlib.RingTheory.AlgebraTower
  {R : Type u_1} {S : Type u_2} {A : Type u_3} [Semiring R] [Semiring S] [AddCommMonoid A] [Module R S] [Module S A] [Module R A] [IsScalarTower R S A] {ι : Type u_5} {ι' : Type u_6} (b : Module.Basis ι R S) (c : Module.Basis ι' S A) (x : A) (i : ι') (j : ι) : ((b.smulTower' c).repr x) (i, j) = (b.repr ((c.repr x) i)) j
• Module.Basis.smulTower_repr_mk 📋 Mathlib.RingTheory.AlgebraTower
  {R : Type u_1} {S : Type u_2} {A : Type u_3} [Semiring R] [Semiring S] [AddCommMonoid A] [Module R S] [Module S A] [Module R A] [IsScalarTower R S A] {ι : Type u_5} {ι' : Type u_6} (b : Module.Basis ι R S) (c : Module.Basis ι' S A) (x : A) (i : ι) (j : ι') : ((b.smulTower c).repr x) (i, j) = (b.repr ((c.repr x) j)) i
• Module.Basis.smulTower'_repr 📋 Mathlib.RingTheory.AlgebraTower
  {R : Type u_1} {S : Type u_2} {A : Type u_3} [Semiring R] [Semiring S] [AddCommMonoid A] [Module R S] [Module S A] [Module R A] [IsScalarTower R S A] {ι : Type u_5} {ι' : Type u_6} (b : Module.Basis ι R S) (c : Module.Basis ι' S A) (x : A) (ij : ι' × ι) : ((b.smulTower' c).repr x) ij = (b.repr ((c.repr x) ij.1)) ij.2
• Module.Basis.smulTower_repr 📋 Mathlib.RingTheory.AlgebraTower
  {R : Type u_1} {S : Type u_2} {A : Type u_3} [Semiring R] [Semiring S] [AddCommMonoid A] [Module R S] [Module S A] [Module R A] [IsScalarTower R S A] {ι : Type u_5} {ι' : Type u_6} (b : Module.Basis ι R S) (c : Module.Basis ι' S A) (x : A) (ij : ι × ι') : ((b.smulTower c).repr x) ij = (b.repr ((c.repr x) ij.2)) ij.1
• Module.basisUnique_repr_eq_zero_iff 📋 Mathlib.LinearAlgebra.Dimension.Free
  {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] [StrongRankCondition R] {ι : Type u_2} [Unique ι] {h : Module.finrank R M = 1} {v : M} {i : ι} : ((Module.basisUnique ι h).repr v) i = 0 ↔ v = 0
• DirectSum.IsInternal.collectedBasis_repr_of_mem_ne 📋 Mathlib.Algebra.DirectSum.Module
  {R : Type u} [Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [AddCommMonoid M] [Module R M] {A : ι → Submodule R M} (h : DirectSum.IsInternal A) {α : ι → Type u_2} (v : (i : ι) → Module.Basis (α i) R ↥(A i)) {x : M} {i j : ι} (hij : i ≠ j) {a : α j} (hx : x ∈ A i) : ((h.collectedBasis v).repr x) ⟨j, a⟩ = 0
• DirectSum.IsInternal.collectedBasis_repr_of_mem 📋 Mathlib.Algebra.DirectSum.Module
  {R : Type u} [Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [AddCommMonoid M] [Module R M] {A : ι → Submodule R M} (h : DirectSum.IsInternal A) {α : ι → Type u_2} (v : (i : ι) → Module.Basis (α i) R ↥(A i)) {x : M} {i : ι} {a : α i} (hx : x ∈ A i) : ((h.collectedBasis v).repr x) ⟨i, a⟩ = ((v i).repr ⟨x, hx⟩) a
• TensorProduct.equivFinsuppOfBasisLeft_apply_tmul_apply 📋 Mathlib.LinearAlgebra.TensorProduct.Basis
  {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [DecidableEq ι] (ℬ : Module.Basis ι R M) (m : M) (n : N) (i : ι) : ((TensorProduct.equivFinsuppOfBasisLeft ℬ) (m ⊗ₜ[R] n)) i = (ℬ.repr m) i • n
• TensorProduct.equivFinsuppOfBasisRight_apply_tmul_apply 📋 Mathlib.LinearAlgebra.TensorProduct.Basis
  {R : Type u_1} {M : Type u_3} {N : Type u_4} {κ : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [DecidableEq κ] (𝒞 : Module.Basis κ R N) (m : M) (n : N) (i : κ) : ((TensorProduct.equivFinsuppOfBasisRight 𝒞) (m ⊗ₜ[R] n)) i = (𝒞.repr n) i • m
• TensorProduct.equivFinsuppOfBasisLeft_apply_tmul 📋 Mathlib.LinearAlgebra.TensorProduct.Basis
  {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [DecidableEq ι] (ℬ : Module.Basis ι R M) (m : M) (n : N) : (TensorProduct.equivFinsuppOfBasisLeft ℬ) (m ⊗ₜ[R] n) = Finsupp.mapRange (fun x => x • n) ⋯ (ℬ.repr m)
• TensorProduct.equivFinsuppOfBasisRight_apply_tmul 📋 Mathlib.LinearAlgebra.TensorProduct.Basis
  {R : Type u_1} {M : Type u_3} {N : Type u_4} {κ : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [DecidableEq κ] (𝒞 : Module.Basis κ R N) (m : M) (n : N) : (TensorProduct.equivFinsuppOfBasisRight 𝒞) (m ⊗ₜ[R] n) = Finsupp.mapRange (fun x => x • m) ⋯ (𝒞.repr n)
• Module.Basis.baseChange_repr_tmul 📋 Mathlib.LinearAlgebra.TensorProduct.Basis
  {R : Type u_1} {M : Type u_3} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] (S : Type u_7) [Semiring S] [Algebra R S] (b : Module.Basis ι R M) (x : S) (y : M) (i : ι) : ((Module.Basis.baseChange S b).repr (x ⊗ₜ[R] y)) i = (b.repr y) i • x
• Module.Basis.tensorProduct_repr_tmul_apply 📋 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 : Module.Basis ι S M) (c : Module.Basis κ R N) (m : M) (n : N) (i : ι) (j : κ) : ((b.tensorProduct c).repr (m ⊗ₜ[R] n)) (i, j) = (c.repr n) j • (b.repr m) i
• Module.Basis.coe_finTwoProd_repr 📋 Mathlib.LinearAlgebra.Basis.Fin
  {R : Type u_7} [Semiring R] (x : R × R) : ⇑((Module.Basis.finTwoProd R).repr x) = ![x.1, x.2]
• Module.Basis.prod_repr_inl 📋 Mathlib.LinearAlgebra.Basis.Prod
  {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_4} {M' : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (b : Module.Basis ι R M) (b' : Module.Basis ι' R M') (x : M × M') (i : ι) : ((b.prod b').repr x) (Sum.inl i) = (b.repr x.1) i
• Module.Basis.prod_repr_inr 📋 Mathlib.LinearAlgebra.Basis.Prod
  {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_4} {M' : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (b : Module.Basis ι R M) (b' : Module.Basis ι' R M') (x : M × M') (i : ι') : ((b.prod b').repr x) (Sum.inr i) = (b'.repr x.2) i
• Module.Basis.repr_smul 📋 Mathlib.LinearAlgebra.Basis.SMul
  {ι : Type u_1} {R : Type u_2} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {G : Type u_5} [Group G] [DistribMulAction G M] [SMulCommClass G R M] (g : G) (b : Module.Basis ι R M) : (g • b).repr = (DistribMulAction.toLinearEquiv R M g).symm ≪≫ₗ b.repr
• Module.Basis.repr_unitsSMul 📋 Mathlib.LinearAlgebra.Basis.SMul
  {ι : Type u_1} {R₂ : Type u_3} {M : Type u_4} [AddCommMonoid M] [CommSemiring R₂] [Module R₂ M] (e : Module.Basis ι R₂ M) (w : ι → R₂ˣ) (v : M) (i : ι) : ((e.unitsSMul w).repr v) i = (w i)⁻¹ • (e.repr v) i
• Module.Basis.repr_isUnitSMul 📋 Mathlib.LinearAlgebra.Basis.SMul
  {ι : Type u_1} {R₂ : Type u_3} {M : Type u_4} [AddCommMonoid M] [CommSemiring R₂] [Module R₂ M] {v : Module.Basis ι R₂ M} {w : ι → R₂} (hw : ∀ (i : ι), IsUnit (w i)) (x : M) (i : ι) : ((v.isUnitSMul hw).repr x) i = ⋯.unit⁻¹ • (v.repr x) i
• Algebra.leftMulMatrix_eq_repr_mul 📋 Mathlib.LinearAlgebra.Matrix.ToLin
  {R : Type u_1} {S : Type u_2} [CommSemiring R] [Semiring S] [Algebra R S] {m : Type u_3} [Fintype m] [DecidableEq m] (b : Module.Basis m R S) (x : S) (i j : m) : (Algebra.leftMulMatrix b) x i j = (b.repr (x * b j)) i
• LinearMap.toMatrixAlgEquiv_apply 📋 Mathlib.LinearAlgebra.Matrix.ToLin
  {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Module.Basis n R M₁) (f : M₁ →ₗ[R] M₁) (i j : n) : (LinearMap.toMatrixAlgEquiv v₁) f i j = (v₁.repr (f (v₁ j))) i
• LinearMap.toMatrixAlgEquiv_apply' 📋 Mathlib.LinearAlgebra.Matrix.ToLin
  {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Module.Basis n R M₁) (f : M₁ →ₗ[R] M₁) (i j : n) : (LinearMap.toMatrixAlgEquiv v₁) f i j = (v₁.repr (f (v₁ j))) i
• LinearMap.toMatrixAlgEquiv_transpose_apply 📋 Mathlib.LinearAlgebra.Matrix.ToLin
  {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Module.Basis n R M₁) (f : M₁ →ₗ[R] M₁) (j : n) : ((LinearMap.toMatrixAlgEquiv v₁) f).transpose j = ⇑(v₁.repr (f (v₁ j)))
• LinearMap.toMatrixAlgEquiv_transpose_apply' 📋 Mathlib.LinearAlgebra.Matrix.ToLin
  {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Module.Basis n R M₁) (f : M₁ →ₗ[R] M₁) (j : n) : ((LinearMap.toMatrixAlgEquiv v₁) f).transpose j = ⇑(v₁.repr (f (v₁ j)))
• Algebra.leftMulMatrix_mulVec_repr 📋 Mathlib.LinearAlgebra.Matrix.ToLin
  {R : Type u_1} {S : Type u_2} [CommSemiring R] [Semiring S] [Algebra R S] {m : Type u_3} [Fintype m] [DecidableEq m] (b : Module.Basis m R S) (x y : S) : ((Algebra.leftMulMatrix b) x).mulVec ⇑(b.repr y) = ⇑(b.repr (x * y))
• Matrix.toLinAlgEquiv_apply 📋 Mathlib.LinearAlgebra.Matrix.ToLin
  {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Module.Basis n R M₁) (M : Matrix n n R) (v : M₁) : ((Matrix.toLinAlgEquiv v₁) M) v = ∑ j, M.mulVec (⇑(v₁.repr v)) j • v₁ j
• LinearMap.toMatrix_apply 📋 Mathlib.LinearAlgebra.Matrix.ToLin
  {R : Type u_1} [CommSemiring R] {m : Type u_3} {n : Type u_4} [Fintype n] [Finite m] [DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (v₁ : Module.Basis n R M₁) (v₂ : Module.Basis m R M₂) (f : M₁ →ₗ[R] M₂) (i : m) (j : n) : (LinearMap.toMatrix v₁ v₂) f i j = (v₂.repr (f (v₁ j))) i
• LinearMap.toMatrix_apply' 📋 Mathlib.LinearAlgebra.Matrix.ToLin
  {R : Type u_1} [CommSemiring R] {m : Type u_3} {n : Type u_4} [Fintype n] [Finite m] [DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (v₁ : Module.Basis n R M₁) (v₂ : Module.Basis m R M₂) (f : M₁ →ₗ[R] M₂) (i : m) (j : n) : (LinearMap.toMatrix v₁ v₂) f i j = (v₂.repr (f (v₁ j))) i
• LinearMap.toMatrix_transpose_apply 📋 Mathlib.LinearAlgebra.Matrix.ToLin
  {R : Type u_1} [CommSemiring R] {m : Type u_3} {n : Type u_4} [Fintype n] [Finite m] [DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (v₁ : Module.Basis n R M₁) (v₂ : Module.Basis m R M₂) (f : M₁ →ₗ[R] M₂) (j : n) : ((LinearMap.toMatrix v₁ v₂) f).transpose j = ⇑(v₂.repr (f (v₁ j)))
• LinearMap.toMatrix_transpose_apply' 📋 Mathlib.LinearAlgebra.Matrix.ToLin
  {R : Type u_1} [CommSemiring R] {m : Type u_3} {n : Type u_4} [Fintype n] [Finite m] [DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (v₁ : Module.Basis n R M₁) (v₂ : Module.Basis m R M₂) (f : M₁ →ₗ[R] M₂) (j : n) : ((LinearMap.toMatrix v₁ v₂) f).transpose j = ⇑(v₂.repr (f (v₁ j)))
• Matrix.toLin_apply 📋 Mathlib.LinearAlgebra.Matrix.ToLin
  {R : Type u_1} [CommSemiring R] {m : Type u_3} {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (v₁ : Module.Basis n R M₁) (v₂ : Module.Basis m R M₂) [Fintype m] (M : Matrix m n R) (v : M₁) : ((Matrix.toLin v₁ v₂) M) v = ∑ j, M.mulVec (⇑(v₁.repr v)) j • v₂ j
• LinearMap.toMatrix_toSpanSingleton 📋 Mathlib.LinearAlgebra.Matrix.ToLin
  {R : Type u_1} [CommSemiring R] {m : Type u_3} {n : Type u_4} [Fintype n] [DecidableEq n] {M₂ : Type u_6} [AddCommMonoid M₂] [Module R M₂] [Finite m] (v₁ : Module.Basis n R R) (v₂ : Module.Basis m R M₂) (x : M₂) : (LinearMap.toMatrix v₁ v₂) (LinearMap.toSpanSingleton R M₂ x) = Matrix.vecMulVec ⇑(v₂.repr x) ⇑v₁
• LinearMap.toMatrix_smulRight 📋 Mathlib.LinearAlgebra.Matrix.ToLin
  {R : Type u_1} [CommSemiring R] {m : Type u_3} {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (v₁ : Module.Basis n R M₁) (v₂ : Module.Basis m R M₂) [Finite m] (f : M₁ →ₗ[R] R) (x : M₂) : (LinearMap.toMatrix v₁ v₂) (f.smulRight x) = Matrix.vecMulVec (⇑(v₂.repr x)) (⇑f ∘ ⇑v₁)
• Matrix.repr_toLin 📋 Mathlib.LinearAlgebra.Matrix.ToLin
  {R : Type u_1} [CommSemiring R] {m : Type u_3} {n : Type u_4} [Fintype n] [Finite m] [DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (v₁ : Module.Basis n R M₁) (v₂ : Module.Basis m R M₂) (M : Matrix m n R) (x : M₁) : ⇑(v₂.repr (((Matrix.toLin v₁ v₂) M) x)) = M.mulVec ⇑(v₁.repr x)
• LinearMap.toMatrix_mulVec_repr 📋 Mathlib.LinearAlgebra.Matrix.ToLin
  {R : Type u_1} [CommSemiring R] {m : Type u_3} {n : Type u_4} [Fintype n] [Finite m] [DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (v₁ : Module.Basis n R M₁) (v₂ : Module.Basis m R M₂) (f : M₁ →ₗ[R] M₂) (x : M₁) : ((LinearMap.toMatrix v₁ v₂) f).mulVec ⇑(v₁.repr x) = ⇑(v₂.repr (f x))
• Matrix.toLin_apply_eq_zero_iff 📋 Mathlib.LinearAlgebra.Matrix.ToLin
  {m : Type u_3} {n : Type u_4} [Fintype n] [DecidableEq n] {R : Type u_7} {M₁ : Type u_8} {M₂ : Type u_9} [Finite m] [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] {v₁ : Module.Basis n R M₁} {v₂ : Module.Basis m R M₂} {A : Matrix m n R} {x : M₁} : ((Matrix.toLin v₁ v₂) A) x = 0 ↔ ∀ (j : m), A.mulVec (⇑(v₁.repr x)) j = 0
• Algebra.toMatrix_lmul' 📋 Mathlib.LinearAlgebra.Matrix.ToLin
  {R : Type u_1} {S : Type u_2} [CommSemiring R] [Semiring S] [Algebra R S] {m : Type u_3} [Fintype m] [DecidableEq m] (b : Module.Basis m R S) (x : S) (i j : m) : (LinearMap.toMatrix b b) ((Algebra.lmul R S) x) i j = (b.repr (x * b j)) i
• Module.Basis.end_repr_apply 📋 Mathlib.LinearAlgebra.Matrix.ToLin
  {R : Type u_1} {M : Type u_2} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [Fintype ι] [DecidableEq ι] (b : Module.Basis ι R M) (x : M →ₗ[R] M) : b.end.repr x = (Matrix.stdBasis R ι ι).repr ((LinearMap.toMatrix b b) x)
• Module.Basis.linearMap_repr_apply 📋 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₁ : Module.Basis ι₁ R M₁) (b₂ : Module.Basis ι₂ R M₂) (x : M₁ →ₗ[R] M₂) : (b₁.linearMap b₂).repr x = (Matrix.stdBasis R ι₂ ι₁).repr ((LinearMap.toMatrix b₁ b₂) x)
• Module.Basis.end_repr_symm_apply 📋 Mathlib.LinearAlgebra.Matrix.ToLin
  {R : Type u_1} {M : Type u_2} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [Fintype ι] [DecidableEq ι] (b : Module.Basis ι R M) (a✝ : ι × ι →₀ R) : b.end.repr.symm a✝ = (Matrix.toLin b b) ((Finsupp.linearCombination R ⇑(Matrix.stdBasis R ι ι)) a✝)
• Module.Basis.linearMap_repr_symm_apply 📋 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₁ : Module.Basis ι₁ R M₁) (b₂ : Module.Basis ι₂ R M₂) (a✝ : ι₂ × ι₁ →₀ R) : (b₁.linearMap b₂).repr.symm a✝ = (Matrix.toLin b₁ b₂) ((Finsupp.linearCombination R ⇑(Matrix.stdBasis R ι₂ ι₁)) a✝)
• Module.Basis.SmithNormalForm.repr_eq_zero_of_notMem_range 📋 Mathlib.LinearAlgebra.FreeModule.PID
  {ι : Type u_1} {R : Type u_2} [CommRing R] {M : Type u_3} [AddCommGroup M] [Module R M] {n : ℕ} {N : Submodule R M} (snf : Module.Basis.SmithNormalForm N ι n) (m : ↥N) {i : ι} (hi : i ∉ Set.range ⇑snf.f) : (snf.bM.repr ↑m) i = 0
• Module.Basis.SmithNormalForm.repr_comp_embedding_eq_smul 📋 Mathlib.LinearAlgebra.FreeModule.PID
  {ι : Type u_1} {R : Type u_2} [CommRing R] {M : Type u_3} [AddCommGroup M] [Module R M] {n : ℕ} {N : Submodule R M} (snf : Module.Basis.SmithNormalForm N ι n) (m : ↥N) : ⇑(snf.bM.repr ↑m) ∘ ⇑snf.f = snf.a • ⇑(snf.bN.repr m)
• Module.Basis.SmithNormalForm.repr_apply_embedding_eq_repr_smul 📋 Mathlib.LinearAlgebra.FreeModule.PID
  {ι : Type u_1} {R : Type u_2} [CommRing R] {M : Type u_3} [AddCommGroup M] [Module R M] {n : ℕ} {N : Submodule R M} (snf : Module.Basis.SmithNormalForm N ι n) (m : ↥N) {i : Fin n} : (snf.bM.repr ↑m) (snf.f i) = (snf.bN.repr (snf.a i • m)) i
• Module.Basis.sumQuot_repr_inr_of_mem 📋 Mathlib.LinearAlgebra.Dimension.Constructions
  {R : Type u_2} {V : Type u_3} [CommRing R] [AddCommGroup V] [Module R V] {W : Submodule R V} {m : Type u_4} {n : Type u_5} (bW : Module.Basis m R ↥W) (bQ : Module.Basis n R (V ⧸ W)) (v : V) (hv : v ∈ W) (j : n) : ((bW.sumQuot bQ).repr v) (Sum.inr j) = 0
• Module.Basis.sumQuot_repr_left 📋 Mathlib.LinearAlgebra.Dimension.Constructions
  {R : Type u_2} {V : Type u_3} [CommRing R] [AddCommGroup V] [Module R V] {W : Submodule R V} {m : Type u_4} {n : Type u_5} (bW : Module.Basis m R ↥W) (bQ : Module.Basis n R (V ⧸ W)) (i : m) : (bW.sumQuot bQ).repr ↑(bW i) = fun₀ | Sum.inl i => 1
• Module.Basis.sumQuot_repr_inr 📋 Mathlib.LinearAlgebra.Dimension.Constructions
  {R : Type u_2} {V : Type u_3} [CommRing R] [AddCommGroup V] [Module R V] {W : Submodule R V} {m : Type u_4} {n : Type u_5} (bW : Module.Basis m R ↥W) (bQ : Module.Basis n R (V ⧸ W)) (v : V) (j : n) : ((bW.sumQuot bQ).repr v) (Sum.inr j) = (bQ.repr (W.mkQ v)) j
• Module.Basis.sumQuot_repr_inl_of_mem 📋 Mathlib.LinearAlgebra.Dimension.Constructions
  {R : Type u_2} {V : Type u_3} [CommRing R] [AddCommGroup V] [Module R V] {W : Submodule R V} {m : Type u_4} {n : Type u_5} (bW : Module.Basis m R ↥W) (bQ : Module.Basis n R (V ⧸ W)) (v : V) (hv : v ∈ W) (i : m) : ((bW.sumQuot bQ).repr v) (Sum.inl i) = (bW.repr ⟨v, hv⟩) i
• Module.Basis.sumQuot_repr_inl 📋 Mathlib.LinearAlgebra.Dimension.Constructions
  {R : Type u_2} {V : Type u_3} [CommRing R] [AddCommGroup V] [Module R V] {W : Submodule R V} {m : Type u_4} {n : Type u_5} (bW : Module.Basis m R ↥W) (bQ : Module.Basis n R (V ⧸ W)) (w : ↥W) (i : m) : ((bW.sumQuot bQ).repr ↑w) (Sum.inl i) = (bW.repr w) i
• FiniteDimensional.basisSingleton_repr_apply 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (ι : Type u_1) [Unique ι] (h : Module.finrank K V = 1) (v : V) (hv : v ≠ 0) (w : V) : (FiniteDimensional.basisSingleton ι h v hv).repr w = fun₀ | default => ((Module.basisUnique ι h).repr w) default / ((Module.basisUnique ι h).repr v) default
• Basis.multilinearMap_apply_apply 📋 Mathlib.LinearAlgebra.Multilinear.Basis
  {ι : Type u_1} {R : Type u_2} [CommSemiring R] {M : ι → Type u_3} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {κ : ι → Type u_5} (b : (i : ι) → Module.Basis (κ i) R (M i)) {ι' : Type u_6} {N : Type u_7} [AddCommMonoid N] [Module R N] (b' : Module.Basis ι' R N) [Fintype ι] [∀ (i : ι), Finite (κ i)] (ii : ((i : ι) → κ i) × ι') (v : (i : ι) → M i) : ((Basis.multilinearMap b b') ii) v = (∏ i, ((b i).repr (v i)) (ii.1 i)) • b' ii.2
• Module.Basis.ofIsLocalizedModule_repr_apply 📋 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) (m : M) (i : ι) : ((Module.Basis.ofIsLocalizedModule Rₛ S f b).repr (f m)) i = (algebraMap R Rₛ) ((b.repr m) i)
• Module.Basis.localizationLocalization_repr_algebraMap 📋 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) (x : A) (i : ι) : ((Module.Basis.localizationLocalization Rₛ S Aₛ b).repr ((algebraMap A Aₛ) x)) i = (algebraMap R Rₛ) ((b.repr x) i)
• Module.DualBases.basis_repr_apply 📋 Mathlib.LinearAlgebra.Dual.Basis
  {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] {e : ι → M} {ε : ι → Module.Dual R M} (h : Module.DualBases e ε) (m : M) : h.basis.repr m = h.coeffs m
• Module.DualBases.basis_repr_symm_apply 📋 Mathlib.LinearAlgebra.Dual.Basis
  {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] {e : ι → M} {ε : ι → Module.Dual R M} (h : Module.DualBases e ε) (l : ι →₀ R) : h.basis.repr.symm l = Module.DualBases.lc e l
• Module.Basis.dualBasis_apply 📋 Mathlib.LinearAlgebra.Dual.Basis
  {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Module.Basis ι R M) [Finite ι] (i : ι) (m : M) : (b.dualBasis i) m = (b.repr m) i
• Module.Basis.toDual_apply_left 📋 Mathlib.LinearAlgebra.Dual.Basis
  {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Module.Basis ι R M) (m : M) (i : ι) : (b.toDual m) (b i) = (b.repr m) i
• Module.Basis.toDual_apply_right 📋 Mathlib.LinearAlgebra.Dual.Basis
  {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Module.Basis ι R M) (i : ι) (m : M) : (b.toDual (b i)) m = (b.repr m) i
• Module.Basis.toDual_eq_repr 📋 Mathlib.LinearAlgebra.Dual.Basis
  {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Module.Basis ι R M) (m : M) (i : ι) : (b.toDual m) (b i) = (b.repr m) i
• Module.Basis.dualBasis_repr 📋 Mathlib.LinearAlgebra.Dual.Basis
  {R : Type uR} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq ι] (b : Module.Basis ι R M) [Finite ι] (l : Module.Dual R M) (i : ι) : (b.dualBasis.repr l) i = l (b i)
• basisOfLinearIndependentOfCardEqFinrank_repr_apply 📋 Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type u_1} [Fintype ι] [Nonempty ι] {b : ι → V} (lin_ind : LinearIndependent K b) (card_eq : Fintype.card ι = Module.finrank K V) (x : V) : (basisOfLinearIndependentOfCardEqFinrank lin_ind card_eq).repr x = lin_ind.repr ((LinearMap.codRestrict (Submodule.span K (Set.range b)) LinearMap.id ⋯) x)
• basisOfLinearIndependentOfCardEqFinrank'_repr_apply 📋 Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type u_1} [Fintype ι] [FiniteDimensional K V] (b : ι → V) (hb : LinearIndependent K b) (hι : Fintype.card ι = Module.finrank K V) (x : V) : (basisOfLinearIndependentOfCardEqFinrank' b hb hι).repr x = hb.repr ((LinearMap.codRestrict (Submodule.span K (Set.range b)) LinearMap.id ⋯) x)
• setBasisOfLinearIndependentOfCardEqFinrank_repr_apply 📋 Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Set V} [Nonempty ↑s] [Fintype ↑s] (lin_ind : LinearIndependent K Subtype.val) (card_eq : s.toFinset.card = Module.finrank K V) (x : V) : (setBasisOfLinearIndependentOfCardEqFinrank lin_ind card_eq).repr x = lin_ind.repr ((LinearMap.codRestrict (Submodule.span K (Set.range Subtype.val)) LinearMap.id ⋯) x)
• finsetBasisOfLinearIndependentOfCardEqFinrank_repr_apply 📋 Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Finset V} (hs : s.Nonempty) (lin_ind : LinearIndependent K Subtype.val) (card_eq : s.card = Module.finrank K V) (x : V) : (finsetBasisOfLinearIndependentOfCardEqFinrank hs lin_ind card_eq).repr x = lin_ind.repr ((LinearMap.codRestrict (Submodule.span K (Set.range Subtype.val)) LinearMap.id ⋯) x)
• Module.Basis.toMatrix_apply 📋 Mathlib.LinearAlgebra.Matrix.Basis
  {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] (e : Module.Basis ι R M) (v : ι' → M) (i : ι) (j : ι') : e.toMatrix v i j = (e.repr (v j)) i
• Module.Basis.toMatrix_transpose_apply 📋 Mathlib.LinearAlgebra.Matrix.Basis
  {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] (e : Module.Basis ι R M) (v : ι' → M) (j : ι') : (e.toMatrix v).transpose j = ⇑(e.repr (v j))
• Module.Basis.toMatrix_update 📋 Mathlib.LinearAlgebra.Matrix.Basis
  {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] (e : Module.Basis ι R M) (v : ι' → M) (j : ι') [DecidableEq ι'] (x : M) : e.toMatrix (Function.update v j x) = (e.toMatrix v).updateCol j ⇑(e.repr x)
• Module.Basis.toMatrix_mulVec_repr 📋 Mathlib.LinearAlgebra.Matrix.Basis
  {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) (b' : Module.Basis ι' R M) [Fintype ι] [Finite ι'] (m : M) : (b'.toMatrix ⇑b).mulVec ⇑(b.repr m) = ⇑(b'.repr m)
• basis_toMatrix_basisFun_mul 📋 Mathlib.LinearAlgebra.Matrix.Basis
  {ι : Type u_1} {R : Type u_5} [CommSemiring R] [Fintype ι] (b : Module.Basis ι R (ι → R)) (A : Matrix ι ι R) : b.toMatrix ⇑(Pi.basisFun R ι) * A = Matrix.of fun i j => (b.repr (A.col j)) i
• Matrix.GeneralLinearGroup.toLin'_apply 📋 Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
  {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] {V : Type u_1} [AddCommGroup V] [Module R V] (b : Module.Basis n R V) (M : GL n R) (v : V) : ((Matrix.GeneralLinearGroup.toLin' b) M).toLinearEquiv v = (Fintype.linearCombination R ⇑b) ((↑M).mulVec ⇑(b.repr v))
• LinearMap.sum_repr_mul_repr_mulₛₗ 📋 Mathlib.LinearAlgebra.Basis.Bilinear
  {ι₁ : Type u_1} {ι₂ : Type u_2} {R : Type u_3} {R₂ : Type u_4} {S : Type u_5} {S₂ : Type u_6} {M : Type u_7} {N : Type u_8} {P : Type u_9} [Semiring R] [Semiring S] [Semiring R₂] [Semiring S₂] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module S N] [Module R₂ P] [Module S₂ P] [SMulCommClass S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} (b₁ : Module.Basis ι₁ R M) (b₂ : Module.Basis ι₂ S N) {B : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P} (x : M) (y : N) : ((b₁.repr x).sum fun i xi => (b₂.repr y).sum fun j yj => ρ₁₂ xi • σ₁₂ yj • (B (b₁ i)) (b₂ j)) = (B x) y
• LinearMap.sum_repr_mul_repr_mul 📋 Mathlib.LinearAlgebra.Basis.Bilinear
  {ι₁ : Type u_1} {ι₂ : Type u_2} {Rₗ : Type u_10} {Mₗ : Type u_11} {Nₗ : Type u_12} {Pₗ : Type u_13} [CommSemiring Rₗ] [AddCommMonoid Mₗ] [AddCommMonoid Nₗ] [AddCommMonoid Pₗ] [Module Rₗ Mₗ] [Module Rₗ Nₗ] [Module Rₗ Pₗ] (b₁' : Module.Basis ι₁ Rₗ Mₗ) (b₂' : Module.Basis ι₂ Rₗ Nₗ) {B : Mₗ →ₗ[Rₗ] Nₗ →ₗ[Rₗ] Pₗ} (x : Mₗ) (y : Nₗ) : ((b₁'.repr x).sum fun i xi => (b₂'.repr y).sum fun j yj => xi • yj • (B (b₁' i)) (b₂' j)) = (B x) y
• Matrix.toLinearMapₛₗ₂_apply 📋 Mathlib.LinearAlgebra.Matrix.SesquilinearForm
  {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {N₂ : Type u_10} {n : Type u_11} {m : Type u_12} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [AddCommMonoid N₂] [Module R N₂] {σ₁ : R →+* R} [Fintype n] [Fintype m] [DecidableEq m] [DecidableEq n] (b₁ : Module.Basis n R M₁) (b₂ : Module.Basis m R M₂) (M : Matrix n m N₂) (x : M₁) (y : M₂) : (((Matrix.toLinearMapₛₗ₂ σ₁ b₁ b₂) M) x) y = ∑ i, ∑ j, σ₁ ((b₁.repr x) i) • (b₂.repr y) j • M i j
• Matrix.toLinearMap₂_apply 📋 Mathlib.LinearAlgebra.Matrix.SesquilinearForm
  {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {N₂ : Type u_10} {n : Type u_11} {m : Type u_12} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [AddCommMonoid N₂] [Module R N₂] [Fintype n] [Fintype m] [DecidableEq m] [DecidableEq n] (b₁ : Module.Basis n R M₁) (b₂ : Module.Basis m R M₂) (M : Matrix n m N₂) (x : M₁) (y : M₂) : (((Matrix.toLinearMap₂ b₁ b₂) M) x) y = ∑ i, ∑ j, (b₁.repr x) i • (b₂.repr y) j • M i j
• apply_eq_dotProduct_toMatrix₂_mulVec 📋 Mathlib.LinearAlgebra.Matrix.SesquilinearForm
  {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {n : Type u_11} {m : Type u_12} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] {σ₁ σ₂ : R →+* R} [Fintype n] [Fintype m] [DecidableEq m] [DecidableEq n] (b₁ : Module.Basis n R M₁) (b₂ : Module.Basis m R M₂) (B : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] R) (x : M₁) (y : M₂) : (B x) y = ⇑σ₁ ∘ ⇑(b₁.repr x) ⬝ᵥ ((LinearMap.toMatrix₂ b₁ b₂) B).mulVec (⇑σ₂ ∘ ⇑(b₂.repr y))
• Algebra.TensorProduct.basisAux_tmul 📋 Mathlib.RingTheory.TensorProduct.Free
  {R : Type u_1} {A : Type u_2} {M : Type uM} {ι : Type uι} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) (a : A) (m : M) : (Algebra.TensorProduct.basisAux A b) (a ⊗ₜ[R] m) = a • Finsupp.mapRange ⇑(algebraMap R A) ⋯ (b.repr m)
• Algebra.TensorProduct.basis_repr_symm_apply 📋 Mathlib.RingTheory.TensorProduct.Free
  {R : Type u_1} {A : Type u_2} {M : Type uM} {ι : Type uι} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) (a : A) (i : ι) : ((Algebra.TensorProduct.basis A b).repr.symm fun₀ | i => a) = a ⊗ₜ[R] b.repr.symm fun₀ | i => 1
• Algebra.TensorProduct.basis_repr_tmul 📋 Mathlib.RingTheory.TensorProduct.Free
  {R : Type u_1} {A : Type u_2} {M : Type uM} {ι : Type uι} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) (a : A) (m : M) : (Algebra.TensorProduct.basis A b).repr (a ⊗ₜ[R] m) = a • Finsupp.mapRange ⇑(algebraMap R A) ⋯ (b.repr m)
• QuaternionAlgebra.coe_basisOneIJK_repr 📋 Mathlib.Algebra.Quaternion
  {R : Type u_3} (c₁ c₂ c₃ : R) [CommRing R] (q : QuaternionAlgebra R c₁ c₂ c₃) : ⇑((QuaternionAlgebra.basisOneIJK c₁ c₂ c₃).repr q) = ![q.re, q.imI, q.imJ, q.imK]
• AdjoinRoot.powerBasisAux'_repr_apply_to_fun 📋 Mathlib.RingTheory.AdjoinRoot
  {R : Type u_1} [CommRing R] {g : Polynomial R} (hg : g.Monic) (f : AdjoinRoot g) (i : Fin g.natDegree) : ((AdjoinRoot.powerBasisAux' hg).repr f) i = ((AdjoinRoot.modByMonicHom hg) f).coeff ↑i
• AdjoinRoot.powerBasisAux'_repr_symm_apply 📋 Mathlib.RingTheory.AdjoinRoot
  {R : Type u_1} [CommRing R] {g : Polynomial R} (hg : g.Monic) (c : Fin g.natDegree →₀ R) : (AdjoinRoot.powerBasisAux' hg).repr.symm c = (AdjoinRoot.mk g) (∑ i, (Polynomial.monomial ↑i) (c i))
• LinearMap.BilinForm.sum_repr_mul_repr_mul 📋 Mathlib.LinearAlgebra.BilinearForm.Hom
  {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {ι : Type u_9} (b : Module.Basis ι R M) (x y : M) : ((b.repr x).sum fun i xi => (b.repr y).sum fun j yj => xi • yj • (B (b i)) (b j)) = (B x) y
• LinearMap.BilinForm.dualBasis_repr_apply 📋 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 : Module.Basis ι K V) (x : V) (i : ι) : ((B.dualBasis hB b).repr x) i = (B x) (b i)
• setBasisOfTopLeSpanOfCardEqFinrank_repr_apply 📋 Mathlib.LinearAlgebra.Dimension.OrzechProperty
  {R : Type u_1} {M : Type u_2} [Semiring R] [OrzechProperty R] [AddCommMonoid M] [Module R M] {s : Set M} [Fintype ↑s] (le_span : ⊤ ≤ Submodule.span R s) (card_eq : s.toFinset.card = Module.finrank R M) (x : M) : (setBasisOfTopLeSpanOfCardEqFinrank le_span card_eq).repr x = ⋯.repr ((LinearMap.codRestrict (Submodule.span R (Set.range Subtype.val)) LinearMap.id ⋯) x)
• finsetBasisOfTopLeSpanOfCardEqFinrank_repr_apply 📋 Mathlib.LinearAlgebra.Dimension.OrzechProperty
  {R : Type u_1} {M : Type u_2} [Semiring R] [OrzechProperty R] [AddCommMonoid M] [Module R M] {s : Finset M} (le_span : ⊤ ≤ Submodule.span R ↑s) (card_eq : s.card = Module.finrank R M) (x : M) : (finsetBasisOfTopLeSpanOfCardEqFinrank le_span card_eq).repr x = ⋯.repr ((LinearMap.codRestrict (Submodule.span R (Set.range Subtype.val)) LinearMap.id ⋯) x)
• RootPairing.Base.toCoweightBasis_repr_coroot 📋 Mathlib.LinearAlgebra.RootSystem.Base
  {ι : 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} (b : P.Base) [P.IsRootSystem] (i : ↥b.support) : b.toCoweightBasis.repr (P.coroot ↑i) = fun₀ | i => 1
• RootPairing.Base.toWeightBasis_repr_root 📋 Mathlib.LinearAlgebra.RootSystem.Base
  {ι : 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} (b : P.Base) [P.IsRootSystem] (i : ↥b.support) : b.toWeightBasis.repr (P.root ↑i) = fun₀ | i => 1
• LinearMap.BilinForm.apply_eq_dotProduct_toMatrix_mulVec 📋 Mathlib.LinearAlgebra.Matrix.BilinearForm
  {R₁ : Type u_1} {M₁ : Type u_2} [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] {n : Type u_5} [Fintype n] [DecidableEq n] (b : Module.Basis n R₁ M₁) (B : LinearMap.BilinForm R₁ M₁) (x y : M₁) : (B x) y = ⇑(b.repr x) ⬝ᵥ ((LinearMap.BilinForm.toMatrix b) B).mulVec ⇑(b.repr y)
• Matrix.toBilin_apply 📋 Mathlib.LinearAlgebra.Matrix.BilinearForm
  {R₁ : Type u_1} {M₁ : Type u_2} [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] {n : Type u_5} [Fintype n] [DecidableEq n] (b : Module.Basis n R₁ M₁) (M : Matrix n n R₁) (x y : M₁) : (((Matrix.toBilin b) M) x) y = ∑ i, ∑ j, (b.repr x) i * M i j * (b.repr y) j
• LinearMap.isNilRegular_iff_coeff_polyCharpoly_nilRank_ne_zero 📋 Mathlib.Algebra.Module.LinearMap.Polynomial
  {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Fintype ι] [DecidableEq ι] [Module.Free R M] [Module.Finite R M] (b : Module.Basis ι R L) [Module.Finite R L] [Module.Free R L] (x : L) : φ.IsNilRegular x ↔ (MvPolynomial.eval ⇑(b.repr x)) ((φ.polyCharpoly b).coeff φ.nilRank) ≠ 0
• LinearMap.polyCharpoly_map_eq_charpoly 📋 Mathlib.Algebra.Module.LinearMap.Polynomial
  {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Fintype ι] [DecidableEq ι] [Module.Free R M] [Module.Finite R M] (b : Module.Basis ι R L) (x : L) : Polynomial.map (MvPolynomial.eval ⇑(b.repr x)) (φ.polyCharpoly b) = LinearMap.charpoly (φ x)
• LinearMap.polyCharpolyAux_map_eq_charpoly 📋 Mathlib.Algebra.Module.LinearMap.Polynomial
  {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} {ιM : Type u_7} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Fintype ι] [Fintype ιM] [DecidableEq ι] [DecidableEq ιM] (b : Module.Basis ι R L) (bₘ : Module.Basis ιM R M) [Module.Finite R M] [Module.Free R M] (x : L) : Polynomial.map (MvPolynomial.eval ⇑(b.repr x)) (φ.polyCharpolyAux b bₘ) = LinearMap.charpoly (φ x)
• LinearMap.polyCharpoly_coeff_eval 📋 Mathlib.Algebra.Module.LinearMap.Polynomial
  {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Fintype ι] [DecidableEq ι] [Module.Free R M] [Module.Finite R M] (b : Module.Basis ι R L) (x : L) (i : ℕ) : (MvPolynomial.eval ⇑(b.repr x)) ((φ.polyCharpoly b).coeff i) = (LinearMap.charpoly (φ x)).coeff i
• LinearMap.polyCharpolyAux_coeff_eval 📋 Mathlib.Algebra.Module.LinearMap.Polynomial
  {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} {ιM : Type u_7} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Fintype ι] [Fintype ιM] [DecidableEq ι] [DecidableEq ιM] (b : Module.Basis ι R L) (bₘ : Module.Basis ιM R M) [Module.Finite R M] [Module.Free R M] (x : L) (i : ℕ) : (MvPolynomial.eval ⇑(b.repr x)) ((φ.polyCharpolyAux b bₘ).coeff i) = (LinearMap.charpoly (φ x)).coeff i
• LinearMap.toMvPolynomial_eval_eq_apply 📋 Mathlib.Algebra.Module.LinearMap.Polynomial
  {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {ι₁ : Type u_4} {ι₂ : Type u_5} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] [Fintype ι₁] [Finite ι₂] [DecidableEq ι₁] (b₁ : Module.Basis ι₁ R M₁) (b₂ : Module.Basis ι₂ R M₂) (f : M₁ →ₗ[R] M₂) (i : ι₂) (c : ι₁ →₀ R) : (MvPolynomial.eval ⇑c) (LinearMap.toMvPolynomial b₁ b₂ f i) = (b₂.repr (f (b₁.repr.symm c))) i
• LinearMap.polyCharpolyAux_map_eval 📋 Mathlib.Algebra.Module.LinearMap.Polynomial
  {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} {ιM : Type u_7} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Fintype ι] [Fintype ιM] [DecidableEq ι] [DecidableEq ιM] (b : Module.Basis ι R L) (bₘ : Module.Basis ιM R M) [Module.Finite R M] [Module.Free R M] (x : ι → R) : Polynomial.map (MvPolynomial.eval x) (φ.polyCharpolyAux b bₘ) = LinearMap.charpoly (φ (b.repr.symm (Finsupp.equivFunOnFinite.symm x)))
• LinearMap.polyCharpolyAux_map_eq_toMatrix_charpoly 📋 Mathlib.Algebra.Module.LinearMap.Polynomial
  {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} {ιM : Type u_7} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Fintype ι] [Fintype ιM] [DecidableEq ι] [DecidableEq ιM] (b : Module.Basis ι R L) (bₘ : Module.Basis ιM R M) (x : L) : Polynomial.map (MvPolynomial.eval ⇑(b.repr x)) (φ.polyCharpolyAux b bₘ) = ((LinearMap.toMatrix bₘ bₘ) (φ x)).charpoly
• LinearMap.polyCharpolyAux_eval_eq_toMatrix_charpoly_coeff 📋 Mathlib.Algebra.Module.LinearMap.Polynomial
  {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} {ιM : Type u_7} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Fintype ι] [Fintype ιM] [DecidableEq ι] [DecidableEq ιM] (b : Module.Basis ι R L) (bₘ : Module.Basis ιM R M) (x : L) (i : ℕ) : (MvPolynomial.eval ⇑(b.repr x)) ((φ.polyCharpolyAux b bₘ).coeff i) = ((LinearMap.toMatrix bₘ bₘ) (φ x)).charpoly.coeff i
• LinearMap.polyCharpolyAux_map_aeval 📋 Mathlib.Algebra.Module.LinearMap.Polynomial
  {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} {ιM : Type u_7} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Fintype ι] [Fintype ιM] [DecidableEq ι] [DecidableEq ιM] (b : Module.Basis ι R L) (bₘ : Module.Basis ιM R M) (A : Type u_8) [CommRing A] [Algebra R A] [Module.Finite A (TensorProduct R A M)] [Module.Free A (TensorProduct R A M)] (x : ι → A) : Polynomial.map (MvPolynomial.aeval x).toRingHom (φ.polyCharpolyAux b bₘ) = ((LinearMap.tensorProduct R A M M ∘ₗ LinearMap.baseChange A φ) ((Algebra.TensorProduct.basis A b).repr.symm (Finsupp.equivFunOnFinite.symm x))).charpoly
• LieAlgebra.isRegular_iff_coeff_polyCharpoly_rank_ne_zero 📋 Mathlib.Algebra.Lie.Rank
  (R : Type u_1) {L : Type u_2} {ι : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Finite R L] [Module.Free R L] [Fintype ι] (b : Module.Basis ι R L) (x : L) [DecidableEq ι] : LieAlgebra.IsRegular R x ↔ (MvPolynomial.eval ⇑(b.repr x)) (((↑(LieAlgebra.ad R L)).polyCharpoly b).coeff (LieAlgebra.rank R L)) ≠ 0
• LieModule.isRegular_iff_coeff_polyCharpoly_rank_ne_zero 📋 Mathlib.Algebra.Lie.Rank
  (R : Type u_1) {L : Type u_2} (M : Type u_3) {ι : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Finite R L] [Module.Free R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module.Finite R M] [Module.Free R M] [Fintype ι] (b : Module.Basis ι R L) (x : L) [DecidableEq ι] : LieModule.IsRegular R M x ↔ (MvPolynomial.eval ⇑(b.repr x)) (((↑(LieModule.toEnd R L M)).polyCharpoly b).coeff (LieModule.rank R L M)) ≠ 0
• LinearRecurrence.repr_basis_apply 📋 Mathlib.Algebra.LinearRecurrence
  {R : Type u_1} [CommSemiring R] (E : LinearRecurrence R) (u : ↥E.solSpace) (n : Fin E.order) : (E.basis.repr u) n = ↑u ↑n
• LinearRecurrence.repr_basis_eq 📋 Mathlib.Algebra.LinearRecurrence
  {R : Type u_1} [CommSemiring R] (E : LinearRecurrence R) (u : ↥E.solSpace) : E.basis.repr u = Finsupp.ofSupportFinite (↑u ∘ Fin.val) ⋯
• KaehlerDifferential.mvPolynomialBasis_repr_D_X 📋 Mathlib.RingTheory.Kaehler.Polynomial
  (R : Type u) [CommRing R] (σ : Type u_1) (i : σ) : (KaehlerDifferential.mvPolynomialBasis R σ).repr ((KaehlerDifferential.D R (MvPolynomial σ R)) (MvPolynomial.X i)) = fun₀ | i => 1
• KaehlerDifferential.mvPolynomialBasis_repr_apply 📋 Mathlib.RingTheory.Kaehler.Polynomial
  (R : Type u) [CommRing R] (σ : Type u_1) (x : MvPolynomial σ R) (i : σ) : ((KaehlerDifferential.mvPolynomialBasis R σ).repr ((KaehlerDifferential.D R (MvPolynomial σ R)) x)) i = (MvPolynomial.pderiv i) x
• KaehlerDifferential.mvPolynomialBasis_repr_symm_single 📋 Mathlib.RingTheory.Kaehler.Polynomial
  (R : Type u) [CommRing R] (σ : Type u_1) (i : σ) (x : MvPolynomial σ R) : ((KaehlerDifferential.mvPolynomialBasis R σ).repr.symm fun₀ | i => x) = x • (KaehlerDifferential.D R (MvPolynomial σ R)) (MvPolynomial.X i)
• KaehlerDifferential.mvPolynomialBasis_repr_D 📋 Mathlib.RingTheory.Kaehler.Polynomial
  (R : Type u) [CommRing R] (σ : Type u_1) (x : MvPolynomial σ R) : (KaehlerDifferential.mvPolynomialBasis R σ).repr ((KaehlerDifferential.D R (MvPolynomial σ R)) x) = (MvPolynomial.mkDerivation R fun x => fun₀ | x => 1) x
• KaehlerDifferential.mvPolynomialBasis_repr_comp_D 📋 Mathlib.RingTheory.Kaehler.Polynomial
  (R : Type u) [CommRing R] (σ : Type u_1) : (↑(KaehlerDifferential.mvPolynomialBasis R σ).repr).compDer (KaehlerDifferential.D R (MvPolynomial σ R)) = MvPolynomial.mkDerivation R fun x => fun₀ | x => 1
• Algebra.Generators.cotangentSpaceBasis_repr_tmul 📋 Mathlib.RingTheory.Extension.Cotangent.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {ι : Type w} (P : Algebra.Generators R S ι) (r : S) (x : P.Ring) (i : ι) : (P.cotangentSpaceBasis.repr (r ⊗ₜ[P.Ring] (KaehlerDifferential.D R P.Ring) x)) i = r * (MvPolynomial.aeval P.val) ((MvPolynomial.pderiv i) x)
• Algebra.Generators.cotangentSpaceBasis_repr_one_tmul 📋 Mathlib.RingTheory.Extension.Cotangent.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {ι : Type w} (P : Algebra.Generators R S ι) (x : P.toExtension.Ring) (i : ι) : (P.cotangentSpaceBasis.repr (1 ⊗ₜ[P.toExtension.Ring] (KaehlerDifferential.D R P.toExtension.Ring) x)) i = (MvPolynomial.aeval P.val) ((MvPolynomial.pderiv i) x)
• Algebra.Generators.repr_CotangentSpaceMap 📋 Mathlib.RingTheory.Extension.Cotangent.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {ι : Type w} {P : Algebra.Generators R S ι} {R' : Type u'} {S' : Type v'} {ι' : Type w'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Generators R' S' ι'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] (f : P.Hom P') (i : ι) (j : ι') : (P'.cotangentSpaceBasis.repr ((Algebra.Extension.CotangentSpace.map f.toExtensionHom) (P.cotangentSpaceBasis i))) j = (MvPolynomial.aeval P'.val) ((MvPolynomial.pderiv j) (f.val i))
• Algebra.Presentation.differentials.comm₂₃ 📋 Mathlib.Algebra.Module.Presentation.Differentials
  {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] (pres : Algebra.Presentation R S ι σ) : pres.toExtension.toKaehler ∘ₗ ↑pres.cotangentSpaceBasis.repr.symm = pres.differentialsSolution.π
• Algebra.Presentation.differentials.comm₂₃' 📋 Mathlib.Algebra.Module.Presentation.Differentials
  {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] (pres : Algebra.Presentation R S ι σ) : pres.toExtension.toKaehler ∘ₗ ↑pres.cotangentSpaceBasis.repr.symm = Finsupp.linearCombination S fun g => (KaehlerDifferential.D R S) (pres.val g)
• Algebra.Presentation.differentials.comm₁₂ 📋 Mathlib.Algebra.Module.Presentation.Differentials
  {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] (pres : Algebra.Presentation R S ι σ) : pres.toExtension.cotangentComplex ∘ₗ Algebra.Presentation.differentials.hom₁ pres = ↑pres.cotangentSpaceBasis.repr.symm ∘ₗ pres.differentialsRelations.map
• Algebra.Presentation.differentials.comm₁₂_single 📋 Mathlib.Algebra.Module.Presentation.Differentials
  {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] (pres : Algebra.Presentation R S ι σ) (r : σ) : pres.toExtension.cotangentComplex ((Algebra.Presentation.differentials.hom₁ pres) fun₀ | r => 1) = pres.cotangentSpaceBasis.repr.symm (pres.differentialsRelations.relation r)
• exteriorPower.basis_repr 📋 Mathlib.LinearAlgebra.ExteriorPower.Basis
  (R : Type u_1) {M : Type u_3} (n : ℕ) [CommRing R] [AddCommGroup M] [Module R M] {I : Type u_5} [LinearOrder I] (b : Module.Basis I R M) (s : ↑(Set.powersetCard I n)) : (Module.Basis.exteriorPower n b).repr (exteriorPower.ιMulti_family R n (⇑b) s) = fun₀ | s => 1
• exteriorPower.basis_repr_self 📋 Mathlib.LinearAlgebra.ExteriorPower.Basis
  (R : Type u_1) {M : Type u_3} (n : ℕ) [CommRing R] [AddCommGroup M] [Module R M] {I : Type u_5} [LinearOrder I] (b : Module.Basis I R M) (s : ↑(Set.powersetCard I n)) : ((Module.Basis.exteriorPower n b).repr (exteriorPower.ιMulti_family R n (⇑b) s)) s = 1
• exteriorPower.basis_repr_ne 📋 Mathlib.LinearAlgebra.ExteriorPower.Basis
  (R : Type u_1) {M : Type u_3} (n : ℕ) [CommRing R] [AddCommGroup M] [Module R M] {I : Type u_5} [LinearOrder I] (b : Module.Basis I R M) {s t : ↑(Set.powersetCard I n)} (hst : s ≠ t) : ((Module.Basis.exteriorPower n b).repr (exteriorPower.ιMulti_family R n (⇑b) s)) t = 0
• exteriorPower.basis_repr_apply 📋 Mathlib.LinearAlgebra.ExteriorPower.Basis
  (R : Type u_1) {M : Type u_3} (n : ℕ) [CommRing R] [AddCommGroup M] [Module R M] {I : Type u_5} [LinearOrder I] (b : Module.Basis I R M) (x : ↥(⋀[R]^n M)) (s : ↑(Set.powersetCard I n)) : ((Module.Basis.exteriorPower n b).repr x) s = (exteriorPower.ιMultiDual R n b s) x
• Algebra.FormallyUnramified.finite_of_free_aux 📋 Mathlib.RingTheory.Unramified.Finite
  {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (I : Type u_4) [DecidableEq I] (b : Module.Basis I R S) (f : I →₀ S) (x : S) (a : I → I →₀ R) (ha : a = fun i => b.repr (b i * x)) : (1 ⊗ₜ[R] x * f.sum fun i y => y ⊗ₜ[R] b i) = ∑ k ∈ f.support.biUnion fun i => (a i).support, (b.repr (f.sum fun i y => (a i) k • y)).sum fun j c => c • b j ⊗ₜ[R] b k
• Algebra.Generators.H1Cotangent.δAux_toAlgHom 📋 Mathlib.RingTheory.Kaehler.JacobiZariski
  {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] [Algebra R S] {T : Type u₃} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] {ι : Type w₁} {ι' : Type w₃} {Q : Algebra.Generators S T ι} {Q' : Algebra.Generators S T ι'} (f : Q.Hom Q') (x : Q.Ring) : (Algebra.Generators.H1Cotangent.δAux R Q') (f.toAlgHom x) = (Algebra.Generators.H1Cotangent.δAux R Q) x + (Finsupp.linearCombination T (⇑(Algebra.Generators.H1Cotangent.δAux R Q') ∘ f.val)) (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (KaehlerDifferential.D S Q.Ring) x))
• Complex.coe_basisOneI_repr 📋 Mathlib.LinearAlgebra.Complex.Module
  (z : ℂ) : ⇑(Complex.basisOneI.repr z) = ![z.re, z.im]
• Module.Basis.equivFunL_apply 📋 Mathlib.Topology.Algebra.Module.FiniteDimension
  {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [CompleteSpace 𝕜] {ι : Type u_1} [Finite ι] [T2Space E] (v : Module.Basis ι 𝕜 E) (x : E) (a✝ : ι) : v.equivFunL x a✝ = (v.repr x) a✝
• Module.Basis.equivFunL_symm_apply_repr 📋 Mathlib.Topology.Algebra.Module.FiniteDimension
  {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [CompleteSpace 𝕜] {ι : Type u_1} [Finite ι] [T2Space E] (v : Module.Basis ι 𝕜 E) (x : E) : v.equivFunL.symm ⇑(v.repr x) = x
• Module.Basis.continuous_coe_repr 📋 Mathlib.Analysis.Normed.Module.FiniteDimension
  {ι : Type u_1} {R : Type u_2} {M : Type u_3} [Finite ι] [NontriviallyNormedField R] [CompleteSpace R] [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [T2Space M] [Module R M] [ContinuousSMul R M] (B : Module.Basis ι R M) : Continuous fun m => ⇑(B.repr m)
• PiLp.basisFun_repr 📋 Mathlib.Analysis.Normed.Lp.PiLp
  (p : ENNReal) (𝕜 : Type u_1) (ι : Type u_2) [Finite ι] [Ring 𝕜] (x : PiLp p fun x => 𝕜) (i : ι) : ((PiLp.basisFun p 𝕜 ι).repr x) i = x.ofLp i
• PiLp.basis_toMatrix_basisFun_mul 📋 Mathlib.Analysis.Normed.Lp.PiLp
  (p : ENNReal) {ι : Type u_2} [Fintype ι] {𝕜 : Type u_5} [SeminormedCommRing 𝕜] (b : Module.Basis ι 𝕜 (PiLp p fun x => 𝕜)) (A : Matrix ι ι 𝕜) : b.toMatrix ⇑(PiLp.basisFun p 𝕜 ι) * A = Matrix.of fun i j => (b.repr (WithLp.toLp p (A.transpose j))) i
• OrthonormalBasis.coe_toBasis_repr_apply 📋 Mathlib.Analysis.InnerProductSpace.PiL2
  {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (x : E) (i : ι) : (b.toBasis.repr x) i = (b.repr x).ofLp i
• InnerProductSpace.toMatrix_rankOne 📋 Mathlib.Analysis.InnerProductSpace.PiL2
  {𝕜 : Type u_7} {E : Type u_8} {F : Type u_9} {ι : Type u_10} {ι' : Type u_11} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [Finite ι] [Fintype ι'] [DecidableEq ι'] (x : E) (y : F) (b : Module.Basis ι 𝕜 E) (b' : OrthonormalBasis ι' 𝕜 F) : (LinearMap.toMatrix b'.toBasis b) ↑(((InnerProductSpace.rankOne 𝕜) x) y) = Matrix.vecMulVec (⇑(b.repr x)) (star (b'.repr y).ofLp)
• parallelepiped_basis_eq 📋 Mathlib.MeasureTheory.Measure.Haar.OfBasis
  {ι : Type u_1} {E : Type u_3} [Fintype ι] [AddCommGroup E] [Module ℝ E] (b : Module.Basis ι ℝ E) : parallelepiped ⇑b = {x | ∀ (i : ι), (b.repr x) i ∈ Set.Icc 0 1}
• ZSpan.mem_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 : Module.Basis ι K E) [LinearOrder K] {m : E} : m ∈ ZSpan.fundamentalDomain b ↔ ∀ (i : ι), (b.repr m) i ∈ Set.Ico 0 1
• ZSpan.repr_fract_apply 📋 Mathlib.Algebra.Module.ZLattice.Basic
  {E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Module.Basis ι K E) [LinearOrder K] [IsStrictOrderedRing K] [FloorRing K] [Fintype ι] (m : E) (i : ι) : (b.repr (ZSpan.fract b m)) i = Int.fract ((b.repr m) i)
• ZSpan.repr_ceil_apply 📋 Mathlib.Algebra.Module.ZLattice.Basic
  {E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Module.Basis ι K E) [LinearOrder K] [IsStrictOrderedRing K] [FloorRing K] [Fintype ι] (m : E) (i : ι) : (b.repr ↑(ZSpan.ceil b m)) i = ↑⌈(b.repr m) i⌉
• ZSpan.repr_floor_apply 📋 Mathlib.Algebra.Module.ZLattice.Basic
  {E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedField K] [NormedAddCommGroup E] [NormedSpace K E] (b : Module.Basis ι K E) [LinearOrder K] [IsStrictOrderedRing K] [FloorRing K] [Fintype ι] (m : E) (i : ι) : (b.repr ↑(ZSpan.floor b m)) i = ↑⌊(b.repr m) i⌋
• Module.Basis.ofZLatticeBasis_repr_apply 📋 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] (L : Submodule ℤ E) [DiscreteTopology ↥L] {ι : Type u_3} [hs : IsZLattice K L] (b : Module.Basis ι ℤ ↥L) (x : ↥L) (i : ι) : ((Module.Basis.ofZLatticeBasis K L b).repr ↑x) i = ↑((b.repr x) i)
• Module.Basis.ofZLatticeComap_repr_apply 📋 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 : Module.Basis ι ℤ ↥L) (x : ↥L) (i : ι) : ((Module.Basis.ofZLatticeComap K L e b).repr ((ZLattice.comap_equiv K L e) x)) i = (b.repr x) i
• InnerProductSpace.gramSchmidt_triangular 📋 Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
  {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [WellFoundedLT ι] {i j : ι} (hij : i < j) (b : Module.Basis ι 𝕜 E) : (b.repr (InnerProductSpace.gramSchmidt 𝕜 (⇑b) i)) j = 0
• ZLattice.normBound_spec 📋 Mathlib.Algebra.Module.ZLattice.Summable
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] {ι : Type u_3} (b : Module.Basis ι ℤ ↥L) (x : ↥L) (i : ι) : ZLattice.normBound b * ↑|(b.repr x) i| ≤ ‖x‖
• ZLattice.abs_repr_le 📋 Mathlib.Algebra.Module.ZLattice.Summable
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] {ι : Type u_3} (b : Module.Basis ι ℤ ↥L) (x : ↥L) (i : ι) : ↑|(b.repr x) i| ≤ (ZLattice.normBound b)⁻¹ * ‖x‖
• ZLattice.exists_forall_abs_repr_le_norm 📋 Mathlib.Algebra.Module.ZLattice.Summable
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] {ι : Type u_2} (b : Module.Basis ι ℤ ↥L) : ∃ ε, 0 < ε ∧ ∀ (x : ↥L) (i : ι), ε * ↑|(b.repr x) i| ≤ ‖x‖
• ZLattice.abs_repr_lt_of_norm_lt 📋 Mathlib.Algebra.Module.ZLattice.Summable
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] {ι : Type u_3} (b : Module.Basis ι ℤ ↥L) (x : ↥L) (n : ℕ) (hxn : ‖x‖ < ZLattice.normBound b * ↑n) (i : ι) : |(b.repr x) i| < ↑n
• ZLattice.le_norm_of_le_abs_repr 📋 Mathlib.Algebra.Module.ZLattice.Summable
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] {ι : Type u_3} (b : Module.Basis ι ℤ ↥L) (x : ↥L) (n : ℕ) (i : ι) (hi : ↑n ≤ |(b.repr x) i|) : ZLattice.normBound b * ↑n ≤ ‖x‖
• QuadraticAlgebra.basis_repr_apply 📋 Mathlib.Algebra.QuadraticAlgebra.Defs
  {R : Type u_1} (a b : R) [Semiring R] (x : QuadraticAlgebra R a b) : ⇑((QuadraticAlgebra.basis a b).repr x) = ![x.re, x.im]
• Module.Basis.traceDual_repr_apply 📋 Mathlib.RingTheory.Trace.Basic
  {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] {ι : Type w} [FiniteDimensional K L] [Algebra.IsSeparable K L] [Finite ι] [DecidableEq ι] (b : Module.Basis ι K L) (x : L) (i : ι) : (b.traceDual.repr x) i = ((Algebra.traceForm K L) x) (b i)

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. 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.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

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. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision 69fae59