Bases indexed by Fin

noncomputable def Module.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), ∀ x ∈ N, c • y + x = 0 → c = 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.

@[simp]

theorem Module.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), ∀ x ∈ N, c • y + x = 0 → c = 0) (hsp : ∀ (z : M), ∃ (c : R), z + c • y ∈ N) : ⇑(mkFinCons y b hli hsp) = Fin.cons y (Subtype.val ∘ ⇑b)

noncomputable def Module.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), ∀ x ∈ N, c • y + x = 0 → c = 0) (hsp : ∀ z ∈ O, ∃ (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.

@[simp]

theorem Module.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), ∀ x ∈ N, c • y + x = 0 → c = 0) (hsp : ∀ z ∈ O, ∃ (c : R), z + c • y ∈ N) : ⇑(mkFinConsOfLE y yO b hNO hli hsp) = Fin.cons ⟨y, yO⟩ (⇑(Submodule.inclusion hNO) ∘ ⇑b)

noncomputable def Module.Basis.mkFinSnoc {R : Type u_3} {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] {n : ℕ} {N : Submodule R M} (b : Basis (Fin n) R ↥N) (y : M) (hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 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.snoc b y.

@[simp]

theorem Module.Basis.coe_mkFinSnoc {R : Type u_3} {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] {n : ℕ} {N : Submodule R M} (b : Basis (Fin n) R ↥N) (y : M) (hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0) (hsp : ∀ (z : M), ∃ (c : R), z + c • y ∈ N) : ⇑(b.mkFinSnoc y hli hsp) = Fin.snoc (Subtype.val ∘ ⇑b) y

noncomputable def Module.Basis.mkFinSnocOfLE {R : Type u_3} {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] {n : ℕ} {N O : Submodule R M} (b : Basis (Fin n) R ↥N) (hNO : N ≤ O) (y : M) (yO : y ∈ O) (hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0) (hsp : ∀ z ∈ O, ∃ (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.snoc b y.

@[simp]

theorem Module.Basis.coe_mkFinSnocOfLE {R : Type u_3} {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] {n : ℕ} {N O : Submodule R M} (b : Basis (Fin n) R ↥N) (hNO : N ≤ O) (y : M) (yO : y ∈ O) (hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0) (hsp : ∀ z ∈ O, ∃ (c : R), z + c • y ∈ N) : ⇑(b.mkFinSnocOfLE hNO y yO hli hsp) = Fin.snoc (⇑(Submodule.inclusion hNO) ∘ ⇑b) ⟨y, yO⟩

noncomputable def Module.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).

@[simp]

theorem Module.Basis.finTwoProd_zero (R : Type u_7) [Semiring R] : (Basis.finTwoProd R) 0 = (1, 0)

@[simp]

theorem Module.Basis.finTwoProd_one (R : Type u_7) [Semiring R] : (Basis.finTwoProd R) 1 = (0, 1)

@[simp]

theorem Module.Basis.coe_finTwoProd_repr {R : Type u_7} [Semiring R] (x : R × R) : ⇑((Basis.finTwoProd R).repr x) = ![x.1, x.2]