Basis.flag_succ

theorem Basis.flag_succ : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {n : ℕ} (b : Basis (Fin n) R M) (k : Fin n), b.flag k.succ = Submodule.span R {b k} ⊔ b.flag k.castSucc

This theorem, `Basis.flag_succ`, states that for any semiring `R`, an additive commutative monoid `M`, a module `M` over `R`, and a natural number `n`, given a basis `b` of `M` indexed by the finite set `Fin n` and an element `k` of `Fin n`, the subspace spanned by the first `k+1` vectors of the basis `b` (denoted as `Basis.flag b (Fin.succ k)`) is equal to the subspace generated by the union of the set containing the `k`-th basis vector and the subspace spanned by the first `k` vectors of the basis `b` (denoted as `Submodule.span R {b k} ⊔ Basis.flag b (Fin.castSucc k)`). Here, `⊔` represents the join operation in the lattice of submodules, which roughly corresponds to the union of sets.

More concisely: For any semiring `R`, additive commutative monoid `M` with `R`-module structure, and finite index set `Fin n`, the subspace spanned by the first `k+1` basis vectors of a basis `b` of `M` is equal to the subspace generated by the `k`-th basis vector and the subspace spanned by the first `k` basis vectors.