Documentation

Mathlib.LinearAlgebra.Basis.Defs

Bases #

This file defines bases in a module or vector space.

It is inspired by Isabelle/HOL's linear algebra, and hence indirectly by HOL Light.

Main definitions #

All definitions are given for families of vectors, i.e. v : ι → M where M is the module or vector space and ι : Type* is an arbitrary indexing type.

Main statements #

Implementation notes #

We use families instead of sets because it allows us to say that two identical vectors are linearly dependent. For bases, this is useful as well because we can easily derive ordered bases by using an ordered index type ι.

Tags #

basis, bases

structure Basis (ι : Type u_1) (R : Type u_3) (M : Type u_6) [Semiring R] [AddCommMonoid M] [Module R M] :
Type (max (max u_1 u_3) u_6)

A Basis ι R M for a module M is the type of ι-indexed R-bases of M.

The basis vectors are available as DFunLike.coe (b : Basis ι R M) : ι → M. To turn a linear independent family of vectors spanning M into a basis, use Basis.mk. They are internally represented as linear equivs M ≃ₗ[R] (ι →₀ R), available as Basis.repr.

  • ofRepr :: (
    • repr : M ≃ₗ[R] ι →₀ R

      repr is the linear equivalence sending a vector x to its coordinates: the cs such that x = ∑ i, c i.

  • )
Instances For
    instance uniqueBasis {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [Subsingleton R] :
    Unique (Basis ι R M)
    Equations
    • uniqueBasis = { default := { repr := default }, uniq := }
    instance Basis.instInhabitedFinsupp {ι : Type u_1} {R : Type u_3} [Semiring R] :
    Inhabited (Basis ι R (ι →₀ R))
    Equations
    theorem Basis.repr_injective {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] :
    instance Basis.instFunLike {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] :
    FunLike (Basis ι R M) ι M

    b i is the ith basis vector.

    Equations
    • Basis.instFunLike = { coe := fun (b : Basis ι R M) (i : ι) => b.repr.symm (Finsupp.single i 1), coe_injective' := }
    @[simp]
    theorem Basis.coe_ofRepr {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (e : M ≃ₗ[R] ι →₀ R) :
    { repr := e } = fun (i : ι) => e.symm (Finsupp.single i 1)
    theorem Basis.injective {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) [Nontrivial R] :
    theorem Basis.repr_symm_single_one {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (i : ι) :
    b.repr.symm (Finsupp.single i 1) = b i
    theorem Basis.repr_symm_single {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (i : ι) (c : R) :
    b.repr.symm (Finsupp.single i c) = c b i
    @[simp]
    theorem Basis.repr_self {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (i : ι) :
    b.repr (b i) = Finsupp.single i 1
    theorem Basis.repr_self_apply {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (i : ι) (j : ι) [Decidable (i = j)] :
    (b.repr (b i)) j = if i = j then 1 else 0
    @[simp]
    theorem Basis.repr_symm_apply {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (v : ι →₀ R) :
    b.repr.symm v = (Finsupp.linearCombination R b) v
    @[simp]
    theorem Basis.coe_repr_symm {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) :
    b.repr.symm = Finsupp.linearCombination R b
    @[simp]
    theorem Basis.repr_linearCombination {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (v : ι →₀ R) :
    b.repr ((Finsupp.linearCombination R b) v) = v
    @[deprecated Basis.repr_linearCombination]
    theorem Basis.repr_total {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (v : ι →₀ R) :
    b.repr ((Finsupp.linearCombination R b) v) = v

    Alias of Basis.repr_linearCombination.

    @[simp]
    theorem Basis.linearCombination_repr {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (x : M) :
    (Finsupp.linearCombination R b) (b.repr x) = x
    @[deprecated Basis.linearCombination_repr]
    theorem Basis.total_repr {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (x : M) :
    (Finsupp.linearCombination R b) (b.repr x) = x

    Alias of Basis.linearCombination_repr.

    theorem Basis.repr_range {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) :
    LinearMap.range b.repr = Finsupp.supported R R Set.univ
    theorem Basis.mem_span_repr_support {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (m : M) :
    m Submodule.span R (b '' (b.repr m).support)
    theorem Basis.repr_support_subset_of_mem_span {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (s : Set ι) {m : M} (hm : m Submodule.span R (b '' s)) :
    (b.repr m).support s
    theorem Basis.mem_span_image {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) {m : M} {s : Set ι} :
    m Submodule.span R (b '' s) (b.repr m).support s
    @[simp]
    theorem Basis.self_mem_span_image {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) [Nontrivial R] {i : ι} {s : Set ι} :
    b i Submodule.span R (b '' s) i s
    @[simp]
    theorem Basis.coord_apply {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (i : ι) :
    ∀ (a : M), (b.coord i) a = (b.repr a) i
    def Basis.coord {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (i : ι) :

    b.coord i is the linear function giving the i'th coordinate of a vector with respect to the basis b.

    b.coord i is an element of the dual space. In particular, for finite-dimensional spaces it is the ιth basis vector of the dual space.

    Equations
    Instances For
      theorem Basis.forall_coord_eq_zero_iff {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) {x : M} :
      (∀ (i : ι), (b.coord i) x = 0) x = 0
      noncomputable def Basis.sumCoords {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) :

      The sum of the coordinates of an element m : M with respect to a basis.

      Equations
      • b.sumCoords = ((Finsupp.lsum ) fun (x : ι) => LinearMap.id) ∘ₗ b.repr
      Instances For
        @[simp]
        theorem Basis.coe_sumCoords {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) :
        b.sumCoords = fun (m : M) => (b.repr m).sum fun (x : ι) => id
        @[simp]
        theorem Basis.coe_sumCoords_of_fintype {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) [Fintype ι] :
        b.sumCoords = (∑ i : ι, b.coord i)
        @[simp]
        theorem Basis.sumCoords_self_apply {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (i : ι) :
        b.sumCoords (b i) = 1
        theorem Basis.dvd_coord_smul {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (i : ι) (m : M) (r : R) :
        r (b.coord i) (r m)
        theorem Basis.coord_repr_symm {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (i : ι) (f : ι →₀ R) :
        (b.coord i) (b.repr.symm f) = f i
        theorem Basis.ext {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) {R₁ : Type u_10} [Semiring R₁] {σ : R →+* R₁} {M₁ : Type u_11} [AddCommMonoid M₁] [Module R₁ M₁] {f₁ : M →ₛₗ[σ] M₁} {f₂ : M →ₛₗ[σ] M₁} (h : ∀ (i : ι), f₁ (b i) = f₂ (b i)) :
        f₁ = f₂

        Two linear maps are equal if they are equal on basis vectors.

        theorem Basis.ext' {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) {R₁ : Type u_10} [Semiring R₁] {σ : R →+* R₁} {σ' : R₁ →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] {M₁ : Type u_11} [AddCommMonoid M₁] [Module R₁ M₁] {f₁ : M ≃ₛₗ[σ] M₁} {f₂ : M ≃ₛₗ[σ] M₁} (h : ∀ (i : ι), f₁ (b i) = f₂ (b i)) :
        f₁ = f₂

        Two linear equivs are equal if they are equal on basis vectors.

        theorem Basis.ext_elem_iff {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) {x : M} {y : M} :
        x = y ∀ (i : ι), (b.repr x) i = (b.repr y) i

        Two elements are equal iff their coordinates are equal.

        theorem Basis.ext_elem {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) {x : M} {y : M} :
        (∀ (i : ι), (b.repr x) i = (b.repr y) i)x = y

        Alias of the reverse direction of Basis.ext_elem_iff.


        Two elements are equal iff their coordinates are equal.

        theorem Basis.repr_eq_iff {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] {b : Basis ι R M} {f : M →ₗ[R] ι →₀ R} :
        b.repr = f ∀ (i : ι), f (b i) = Finsupp.single i 1
        theorem Basis.repr_eq_iff' {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] {b : Basis ι R M} {f : M ≃ₗ[R] ι →₀ R} :
        b.repr = f ∀ (i : ι), f (b i) = Finsupp.single i 1
        theorem Basis.apply_eq_iff {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] {b : Basis ι R M} {x : M} {i : ι} :
        b i = x b.repr x = Finsupp.single i 1
        theorem Basis.repr_apply_eq {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : 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) = (Finsupp.single i 1)) (x : M) (i : ι) :
        (b.repr x) i = f x i

        An unbundled version of repr_eq_iff

        theorem Basis.eq_ofRepr_eq_repr {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] {b₁ : Basis ι R M} {b₂ : Basis ι R M} (h : ∀ (x : M) (i : ι), (b₁.repr x) i = (b₂.repr x) i) :
        b₁ = b₂

        Two bases are equal if they assign the same coordinates.

        theorem Basis.eq_of_apply_eq_iff {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] {b₁ : Basis ι R M} {b₂ : Basis ι R M} :
        b₁ = b₂ ∀ (i : ι), b₁ i = b₂ i
        theorem Basis.eq_of_apply_eq {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] {b₁ : Basis ι R M} {b₂ : Basis ι R M} :
        (∀ (i : ι), b₁ i = b₂ i)b₁ = b₂

        Two bases are equal if their basis vectors are the same.

        @[simp]
        theorem Basis.map_repr {ι : 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
        def Basis.map {ι : 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'

        Apply the linear equivalence f to the basis vectors.

        Equations
        • b.map f = { repr := f.symm ≪≫ₗ b.repr }
        Instances For
          @[simp]
          theorem Basis.map_apply {ι : 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)
          theorem Basis.coe_map {ι : 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
          instance Basis.instSMul {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] {G : Type u_10} [Group G] [DistribMulAction G M] [SMulCommClass G R M] :
          SMul G (Basis ι R M)

          The action on a Basis by acting on each element.

          See also Basis.unitsSMul and Basis.groupSMul, for the cases when a different action is applied to each basis element.

          Equations
          @[simp]
          theorem Basis.smul_apply {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] {G : Type u_10} [Group G] [DistribMulAction G M] [SMulCommClass G R M] (g : G) (b : Basis ι R M) (i : ι) :
          (g b) i = g b i
          theorem Basis.coe_smul {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] {G : Type u_10} [Group G] [DistribMulAction G M] [SMulCommClass G R M] (g : G) (b : Basis ι R M) :
          (g b) = g b
          @[simp]
          theorem Basis.smul_eq_map {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (g : M ≃ₗ[R] M) (b : Basis ι R M) :
          g b = b.map g

          When the group in question is the automorphisms, coincides with Basis.map.

          @[simp]
          theorem Basis.repr_smul {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] {G : Type u_10} [Group G] [DistribMulAction G M] [SMulCommClass G R M] (g : G) (b : Basis ι R M) :
          (g b).repr = (DistribMulAction.toLinearEquiv R M g).symm ≪≫ₗ b.repr
          instance Basis.instMulAction {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] {G : Type u_10} [Group G] [DistribMulAction G M] [SMulCommClass G R M] :
          MulAction G (Basis ι R M)
          Equations
          instance Basis.instSMulCommClass {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] {G : Type u_10} {G' : Type u_11} [Group G] [Group G'] [DistribMulAction G M] [DistribMulAction G' M] [SMulCommClass G R M] [SMulCommClass G' R M] [SMulCommClass G G' M] :
          SMulCommClass G G' (Basis ι R M)
          Equations
          • =
          instance Basis.instIsScalarTower {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] {G : Type u_10} {G' : Type u_11} [Group G] [Group G'] [DistribMulAction G M] [DistribMulAction G' M] [SMulCommClass G R M] [SMulCommClass G' R M] [SMul G G'] [IsScalarTower G G' M] :
          IsScalarTower G G' (Basis ι R M)
          Equations
          • =
          @[simp]
          theorem Basis.mapCoeffs_repr {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : 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
          def Basis.mapCoeffs {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : 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) :
          Basis ι R' M

          If R and R' are isomorphic rings that act identically on a module M, then a basis for M as R-module is also a basis for M as R'-module.

          See also Basis.algebraMapCoeffs for the case where f is equal to algebraMap.

          Equations
          Instances For
            theorem Basis.mapCoeffs_apply {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : 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) (i : ι) :
            (b.mapCoeffs f h) i = b i
            @[simp]
            theorem Basis.coe_mapCoeffs {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : 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) = b
            def Basis.reindex {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (e : ι ι') :
            Basis ι' R M

            b.reindex (e : ι ≃ ι') is a basis indexed by ι'

            Equations
            Instances For
              theorem Basis.reindex_apply {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (e : ι ι') (i' : ι') :
              (b.reindex e) i' = b (e.symm i')
              @[simp]
              theorem Basis.coe_reindex {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (e : ι ι') :
              (b.reindex e) = b e.symm
              theorem Basis.repr_reindex_apply {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (x : M) (e : ι ι') (i' : ι') :
              ((b.reindex e).repr x) i' = (b.repr x) (e.symm i')
              @[simp]
              theorem Basis.repr_reindex {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (x : M) (e : ι ι') :
              (b.reindex e).repr x = Finsupp.mapDomain (⇑e) (b.repr x)
              @[simp]
              theorem Basis.reindex_refl {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) :
              b.reindex (Equiv.refl ι) = b
              theorem Basis.range_reindex {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (e : ι ι') :
              Set.range (b.reindex e) = Set.range b

              simp can prove this as Basis.coe_reindex + EquivLike.range_comp

              @[simp]
              theorem Basis.sumCoords_reindex {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (e : ι ι') :
              (b.reindex e).sumCoords = b.sumCoords
              def Basis.reindexRange {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) :
              Basis (↑(Set.range b)) R M

              b.reindex_range is a basis indexed by range b, the basis vectors themselves.

              Equations
              Instances For
                theorem Basis.reindexRange_self {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (i : ι) (h : optParam (b i Set.range b) ) :
                b.reindexRange b i, h = b i
                theorem Basis.reindexRange_repr_self {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (i : ι) :
                b.reindexRange.repr (b i) = Finsupp.single b i, 1
                @[simp]
                theorem Basis.reindexRange_apply {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (x : (Set.range b)) :
                b.reindexRange x = x
                theorem Basis.reindexRange_repr' {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (x : M) {bi : M} {i : ι} (h : b i = bi) :
                (b.reindexRange.repr x) bi, = (b.repr x) i
                @[simp]
                theorem Basis.reindexRange_repr {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (x : M) (i : ι) (h : optParam (b i Set.range b) ) :
                (b.reindexRange.repr x) b i, h = (b.repr x) i
                def Basis.reindexFinsetRange {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) [Fintype ι] [DecidableEq M] :
                Basis { x : M // x Finset.image (⇑b) Finset.univ } R M

                b.reindexFinsetRange is a basis indexed by Finset.univ.image b, the finite set of basis vectors themselves.

                Equations
                • b.reindexFinsetRange = b.reindexRange.reindex ((Equiv.refl M).subtypeEquiv )
                Instances For
                  theorem Basis.reindexFinsetRange_self {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) [Fintype ι] [DecidableEq M] (i : ι) (h : optParam (b i Finset.image (⇑b) Finset.univ) ) :
                  b.reindexFinsetRange b i, h = b i
                  @[simp]
                  theorem Basis.reindexFinsetRange_apply {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) [Fintype ι] [DecidableEq M] (x : { x : M // x Finset.image (⇑b) Finset.univ }) :
                  b.reindexFinsetRange x = x
                  theorem Basis.reindexFinsetRange_repr_self {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) [Fintype ι] [DecidableEq M] (i : ι) :
                  b.reindexFinsetRange.repr (b i) = Finsupp.single b i, 1
                  @[simp]
                  theorem Basis.reindexFinsetRange_repr {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) [Fintype ι] [DecidableEq M] (x : M) (i : ι) (h : optParam (b i Finset.image (⇑b) Finset.univ) ) :
                  (b.reindexFinsetRange.repr x) b i, h = (b.repr x) i
                  theorem Basis.mem_span {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (x : M) :
                  @[simp]
                  theorem Basis.span_eq {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) :
                  theorem Basis.index_nonempty {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) [Nontrivial M] :
                  theorem Basis.mem_submodule_iff {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] {P : Submodule R M} (b : Basis ι R P) {x : M} :
                  x P ∃ (c : ι →₀ R), x = c.sum fun (i : ι) (x : R) => x (b i)

                  If the submodule P has a basis, x ∈ P iff it is a linear combination of basis vectors.

                  def Basis.constr {ι : 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) (S : Type u_10) [Semiring S] [Module S M'] [SMulCommClass R S M'] :
                  (ιM') ≃ₗ[S] M →ₗ[R] M'

                  Construct a linear map given the value at the basis, called Basis.constr b S f where b is a basis, f is the value of the linear map over the elements of the basis, and S is an extra semiring (typically S = R or S = ℕ).

                  This definition is parameterized over an extra Semiring S, such that SMulCommClass R S M' holds. If R is commutative, you can set S := R; if R is not commutative, you can recover an AddEquiv by setting S := ℕ. See library note [bundled maps over different rings].

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    theorem Basis.constr_def {ι : 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) (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
                    theorem Basis.constr_apply {ι : 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) (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 : R) => a f b
                    @[simp]
                    theorem Basis.constr_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) (S : Type u_10) [Semiring S] [Module S M'] [SMulCommClass R S M'] (f : ιM') (i : ι) :
                    ((b.constr S) f) (b i) = f i
                    theorem Basis.constr_eq {ι : 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) (S : Type u_10) [Semiring S] [Module S M'] [SMulCommClass R S M'] {g : ιM'} {f : M →ₗ[R] M'} (h : ∀ (i : ι), g i = f (b i)) :
                    (b.constr S) g = f
                    theorem Basis.constr_self {ι : 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) (S : Type u_10) [Semiring S] [Module S M'] [SMulCommClass R S M'] (f : M →ₗ[R] M') :
                    ((b.constr S) fun (i : ι) => f (b i)) = f
                    theorem Basis.constr_range {ι : 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) (S : Type u_10) [Semiring S] [Module S M'] [SMulCommClass R S M'] {f : ιM'} :
                    LinearMap.range ((b.constr S) f) = Submodule.span R (Set.range f)
                    @[simp]
                    theorem Basis.constr_comp {ι : 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) (S : Type u_10) [Semiring S] [Module S M'] [SMulCommClass R S M'] (f : M' →ₗ[R] M') (v : ιM') :
                    (b.constr S) (f v) = f ∘ₗ (b.constr S) v
                    def Basis.equiv {ι : Type u_1} {ι' : Type u_2} {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) (b' : Basis ι' R M') (e : ι ι') :
                    M ≃ₗ[R] M'

                    If b is a basis for M and b' a basis for M', and the index types are equivalent, b.equiv b' e is a linear equivalence M ≃ₗ[R] M', mapping b i to b' (e i).

                    Equations
                    • b.equiv b' e = b.repr ≪≫ₗ (b'.reindex e.symm).repr.symm
                    Instances For
                      @[simp]
                      theorem Basis.equiv_apply {ι : Type u_1} {ι' : Type u_2} {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) (i : ι) (b' : Basis ι' R M') (e : ι ι') :
                      (b.equiv b' e) (b i) = b' (e i)
                      @[simp]
                      theorem Basis.equiv_refl {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) :
                      b.equiv b (Equiv.refl ι) = LinearEquiv.refl R M
                      @[simp]
                      theorem Basis.equiv_symm {ι : Type u_1} {ι' : Type u_2} {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) (b' : Basis ι' R M') (e : ι ι') :
                      (b.equiv b' e).symm = b'.equiv b e.symm
                      @[simp]
                      theorem Basis.equiv_trans {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_6} {M' : Type u_7} {M'' : Type u_8} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (b : Basis ι R M) (b' : Basis ι' R M') [AddCommMonoid M''] [Module R M''] {ι'' : Type u_10} (b'' : Basis ι'' R M'') (e : ι ι') (e' : ι' ι'') :
                      b.equiv b' e ≪≫ₗ b'.equiv b'' e' = b.equiv b'' (e.trans e')
                      @[simp]
                      theorem Basis.map_equiv {ι : Type u_1} {ι' : Type u_2} {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) (b' : Basis ι' R M') (e : ι ι') :
                      b.map (b.equiv b' e) = b'.reindex e.symm
                      def Basis.singleton (ι : Type u_10) (R : Type u_11) [Unique ι] [Semiring R] :
                      Basis ι R R

                      Basis.singleton ι R is the basis sending the unique element of ι to 1 : R.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        @[simp]
                        theorem Basis.singleton_apply (ι : Type u_10) (R : Type u_11) [Unique ι] [Semiring R] (i : ι) :
                        (Basis.singleton ι R) i = 1
                        @[simp]
                        theorem Basis.singleton_repr (ι : Type u_10) (R : Type u_11) [Unique ι] [Semiring R] (x : R) (i : ι) :
                        ((Basis.singleton ι R).repr x) i = x
                        def Basis.empty {ι : Type u_1} {R : Type u_3} (M : Type u_6) [Semiring R] [AddCommMonoid M] [Module R M] [Subsingleton M] [IsEmpty ι] :
                        Basis ι R M

                        If M is a subsingleton and ι is empty, this is the unique ι-indexed basis for M.

                        Equations
                        Instances For
                          instance Basis.emptyUnique {ι : Type u_1} {R : Type u_3} (M : Type u_6) [Semiring R] [AddCommMonoid M] [Module R M] [Subsingleton M] [IsEmpty ι] :
                          Unique (Basis ι R M)
                          Equations
                          def Basis.equivFun {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [Finite ι] (b : Basis ι R M) :
                          M ≃ₗ[R] ιR

                          A module over R with a finite basis is linearly equivalent to functions from its basis to R.

                          Equations
                          • b.equivFun = b.repr ≪≫ₗ let __src := Finsupp.equivFunOnFinite; { toFun := DFunLike.coe, map_add' := , map_smul' := , invFun := __src.invFun, left_inv := , right_inv := }
                          Instances For
                            def Module.fintypeOfFintype {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [Fintype ι] (b : Basis ι R M) [Fintype R] :

                            A module over a finite ring that admits a finite basis is finite.

                            Equations
                            Instances For
                              theorem Module.card_fintype {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [Fintype ι] (b : Basis ι R M) [Fintype R] [Fintype M] :
                              @[simp]
                              theorem Basis.equivFun_symm_apply {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [Fintype ι] (b : Basis ι R M) (x : ιR) :
                              b.equivFun.symm x = i : ι, x i b i

                              Given a basis v indexed by ι, the canonical linear equivalence between ι → R and M maps a function x : ι → R to the linear combination ∑_i x i • v i.

                              @[simp]
                              theorem Basis.equivFun_apply {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [Finite ι] (b : Basis ι R M) (u : M) :
                              b.equivFun u = (b.repr u)
                              @[simp]
                              theorem Basis.map_equivFun {ι : 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
                              theorem Basis.sum_equivFun {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [Fintype ι] (b : Basis ι R M) (u : M) :
                              i : ι, b.equivFun u i b i = u
                              theorem Basis.sum_repr {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [Fintype ι] (b : Basis ι R M) (u : M) :
                              i : ι, (b.repr u) i b i = u
                              @[simp]
                              theorem Basis.equivFun_self {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [Finite ι] [DecidableEq ι] (b : Basis ι R M) (i : ι) (j : ι) :
                              b.equivFun (b i) j = if i = j then 1 else 0
                              theorem Basis.repr_sum_self {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [Fintype ι] (b : Basis ι R M) (c : ιR) :
                              (b.repr (∑ i : ι, c i b i)) = c
                              def Basis.ofEquivFun {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [Finite ι] (e : M ≃ₗ[R] ιR) :
                              Basis ι R M

                              Define a basis by mapping each vector x : M to its coordinates e x : ι → R, as long as ι is finite.

                              Equations
                              Instances For
                                @[simp]
                                theorem Basis.ofEquivFun_repr_apply {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [Finite ι] (e : M ≃ₗ[R] ιR) (x : M) (i : ι) :
                                ((Basis.ofEquivFun e).repr x) i = e x i
                                @[simp]
                                theorem Basis.coe_ofEquivFun {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [Finite ι] [DecidableEq ι] (e : M ≃ₗ[R] ιR) :
                                (Basis.ofEquivFun e) = fun (i : ι) => e.symm (Pi.single i 1)
                                @[simp]
                                theorem Basis.ofEquivFun_equivFun {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [Finite ι] (v : Basis ι R M) :
                                Basis.ofEquivFun v.equivFun = v
                                @[simp]
                                theorem Basis.equivFun_ofEquivFun {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [Finite ι] (e : M ≃ₗ[R] ιR) :
                                (Basis.ofEquivFun e).equivFun = e
                                @[simp]
                                theorem Basis.constr_apply_fintype {ι : 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'] (S : Type u_10) [Semiring S] [Module S M'] [SMulCommClass R S M'] [Fintype ι] (b : Basis ι R M) (f : ιM') (x : M) :
                                ((b.constr S) f) x = i : ι, b.equivFun x i f i
                                theorem Basis.mem_submodule_iff' {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [Fintype ι] {P : Submodule R M} (b : Basis ι R P) {x : M} :
                                x P ∃ (c : ιR), x = i : ι, c i (b i)

                                If the submodule P has a finite basis, x ∈ P iff it is a linear combination of basis vectors.

                                theorem Basis.coord_equivFun_symm {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [Finite ι] (b : Basis ι R M) (i : ι) (f : ιR) :
                                (b.coord i) (b.equivFun.symm f) = f i
                                def Basis.equiv' {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_6} {M' : Type u_7} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (b : Basis ι R M) (b' : Basis ι' R M') (f : MM') (g : M'M) (hf : ∀ (i : ι), f (b i) Set.range b') (hg : ∀ (i : ι'), g (b' i) Set.range b) (hgf : ∀ (i : ι), g (f (b i)) = b i) (hfg : ∀ (i : ι'), f (g (b' i)) = b' i) :
                                M ≃ₗ[R] M'

                                If b is a basis for M and b' a basis for M', and f, g form a bijection between the basis vectors, b.equiv' b' f g hf hg hgf hfg is a linear equivalence M ≃ₗ[R] M', mapping b i to f (b i).

                                Equations
                                • b.equiv' b' f g hf hg hgf hfg = { toLinearMap := (b.constr R) (f b), invFun := ((b'.constr R) (g b')), left_inv := , right_inv := }
                                Instances For
                                  @[simp]
                                  theorem Basis.equiv'_apply {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_6} {M' : Type u_7} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (b : Basis ι R M) (b' : Basis ι' R M') (f : MM') (g : M'M) (hf : ∀ (i : ι), f (b i) Set.range b') (hg : ∀ (i : ι'), g (b' i) Set.range b) (hgf : ∀ (i : ι), g (f (b i)) = b i) (hfg : ∀ (i : ι'), f (g (b' i)) = b' i) (i : ι) :
                                  (b.equiv' b' f g hf hg hgf hfg) (b i) = f (b i)
                                  @[simp]
                                  theorem Basis.equiv'_symm_apply {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_6} {M' : Type u_7} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (b : Basis ι R M) (b' : Basis ι' R M') (f : MM') (g : M'M) (hf : ∀ (i : ι), f (b i) Set.range b') (hg : ∀ (i : ι'), g (b' i) Set.range b) (hgf : ∀ (i : ι), g (f (b i)) = b i) (hfg : ∀ (i : ι'), f (g (b' i)) = b' i) (i : ι') :
                                  (b.equiv' b' f g hf hg hgf hfg).symm (b' i) = g (b' i)
                                  theorem Basis.sum_repr_mul_repr {ι : Type u_1} {R : Type u_3} {M : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) {ι' : Type u_10} [Fintype ι'] (b' : Basis ι' R M) (x : M) (i : ι) :
                                  j : ι', (b.repr (b' j)) i * (b'.repr x) j = (b.repr x) i