Documentation

Mathlib.LinearAlgebra.Basis.Fin

Bases indexed by Fin #

noncomputable def Basis.mkFinCons {R : Type u_3} {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] {n : } {N : Submodule R M} (y : M) (b : Basis (Fin n) R N) (hli : ∀ (c : R), xN, c y + x = 0c = 0) (hsp : ∀ (z : M), ∃ (c : R), z + c y N) :
Basis (Fin (n + 1)) R M

Let b be a basis for a submodule N of M. If y : M is linear independent of N and y and N together span the whole of M, then there is a basis for M whose basis vectors are given by Fin.cons y b.

Equations
    Instances For
      @[simp]
      theorem Basis.coe_mkFinCons {R : Type u_3} {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] {n : } {N : Submodule R M} (y : M) (b : Basis (Fin n) R N) (hli : ∀ (c : R), xN, c y + x = 0c = 0) (hsp : ∀ (z : M), ∃ (c : R), z + c y N) :
      (mkFinCons y b hli hsp) = Fin.cons y (Subtype.val b)
      noncomputable def Basis.mkFinConsOfLE {R : Type u_3} {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] {n : } {N O : Submodule R M} (y : M) (yO : y O) (b : Basis (Fin n) R N) (hNO : N O) (hli : ∀ (c : R), xN, c y + x = 0c = 0) (hsp : zO, ∃ (c : R), z + c y N) :
      Basis (Fin (n + 1)) R O

      Let b be a basis for a submodule N ≤ O. If y ∈ O is linear independent of N and y and N together span the whole of O, then there is a basis for O whose basis vectors are given by Fin.cons y b.

      Equations
        Instances For
          @[simp]
          theorem Basis.coe_mkFinConsOfLE {R : Type u_3} {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] {n : } {N O : Submodule R M} (y : M) (yO : y O) (b : Basis (Fin n) R N) (hNO : N O) (hli : ∀ (c : R), xN, c y + x = 0c = 0) (hsp : zO, ∃ (c : R), z + c y N) :
          (mkFinConsOfLE y yO b hNO hli hsp) = Fin.cons y, yO ((Submodule.inclusion hNO) b)
          def Basis.finTwoProd (R : Type u_7) [Semiring R] :
          Basis (Fin 2) R (R × R)

          The basis of R × R given by the two vectors (1, 0) and (0, 1).

          Equations
            Instances For
              @[simp]
              theorem Basis.finTwoProd_zero (R : Type u_7) [Semiring R] :
              @[simp]
              theorem Basis.finTwoProd_one (R : Type u_7) [Semiring R] :
              @[simp]
              theorem Basis.coe_finTwoProd_repr {R : Type u_7} [Semiring R] (x : R × R) :
              ((Basis.finTwoProd R).repr x) = ![x.1, x.2]