exists_linearIndependent_snoc_of_lt_finrank
theorem exists_linearIndependent_snoc_of_lt_finrank :
∀ {R : Type u_1} {M : Type u} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : HasRankNullity.{u, u_1} R] [inst_4 : StrongRankCondition R] {n : ℕ} {v : Fin n → M},
LinearIndependent R v → n < FiniteDimensional.finrank R M → ∃ x, LinearIndependent R (Fin.snoc v x)
This theorem states that given a family of `n` linearly independent vectors in a finite-dimensional space of dimension greater than `n` over a ring `R` (with the module structure and notions of rank and nullity), you can always add another vector to this family such that the extended family (original vectors plus the new one) stays linearly independent. This essentially says that an `n`-dimensional subspace of a finite-dimensional space of higher dimension can always be extended by adding a new vector.
More concisely: Given a finite-dimensional vector space over a ring with dimension greater than the number of linearly independent vectors in a subset, there exists a vector that can be added to the subset to maintain linear independence.
|
rank_range_add_rank_ker
theorem rank_range_add_rank_ker :
∀ {R : Type u_1} {M M₁ : Type u} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup M₁]
[inst_3 : Module R M] [inst_4 : Module R M₁] [inst_5 : HasRankNullity.{u, u_1} R] (f : M →ₗ[R] M₁),
Module.rank R ↥(LinearMap.range f) + Module.rank R ↥(LinearMap.ker f) = Module.rank R M
This theorem is a formal statement of the rank-nullity theorem in the context of linear algebra. It states that for any linear map `f` from a module `M` to a module `M₁` over a ring `R`, the sum of the ranks of the image (range) and the kernel of `f` is equal to the rank of `M`. This is a foundational result in linear algebra, connecting the dimensions of these three fundamental spaces associated with a linear transformation.
More concisely: For any linear map between modules, the sum of the ranks of its kernel and image equals the rank of the domain module.
|
exists_linearIndependent_snoc_of_lt_rank
theorem exists_linearIndependent_snoc_of_lt_rank :
∀ {R : Type u_1} {M : Type u} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : HasRankNullity.{u, u_1} R] [inst_4 : StrongRankCondition R] {n : ℕ} {v : Fin n → M},
LinearIndependent R v → ↑n < Module.rank R M → ∃ x, LinearIndependent R (Fin.snoc v x)
This theorem states that given a family of `n` linearly independent vectors, denoted by `v`, in a vector space `M` over a ring `R`, if the rank of the vector space is greater than `n`, then there exists a vector `x` such that adding `x` to the family `v` (using the `Fin.snoc` function to append `x` to the end of `v`) still results in a linearly independent family of vectors. The ring `R` is assumed to satisfy the rank-nullity theorem and the strong rank condition.
More concisely: Given a linearly independent family `v` of size `n` in a finite-dimensional vector space `M` over a ring `R` satisfying the rank-nullity theorem and the strong rank condition, if the rank of `M` is greater than `n`, then there exists a linearly independent vector `x` such that `v ∪ {x}` is also linearly independent.
|
exists_linearIndependent_cons_of_lt_rank
theorem exists_linearIndependent_cons_of_lt_rank :
∀ {R : Type u_1} {M : Type u} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : HasRankNullity.{u, u_1} R] [inst_4 : StrongRankCondition R] {n : ℕ} {v : Fin n → M},
LinearIndependent R v → ↑n < Module.rank R M → ∃ x, LinearIndependent R (Fin.cons x v)
The theorem `exists_linearIndependent_cons_of_lt_rank` states that given a collection of `n` linearly independent vectors (denoted by `v`) in a vector space over a ring `R` (with `AddCommGroup` structure denoted by `M` and `Module` structure), if the rank of the module is greater than `n`, then it is possible to add another vector `x` to the collection `v` (using the `Fin.cons` operation) such that the extended family of vectors remains linearly independent. This statement is under the assumption of the `HasRankNullity` and `StrongRankCondition` of the ring `R`.
More concisely: Given a linearly independent set of vectors `v` in an `n`-dimensional vector space over a ring `R` with `AddCommGroup` and `Module` structures satisfying the `HasRankNullity` and `StrongRankCondition`, if the rank of the vector space is greater than `n`, then there exists a vector `x` such that `v ⊕ {x}` is also linearly independent.
|
exists_linearIndependent_pair_of_one_lt_finrank
theorem exists_linearIndependent_pair_of_one_lt_finrank :
∀ {R : Type u_1} {M : Type u} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : HasRankNullity.{u, u_1} R] [inst_4 : StrongRankCondition R] [inst_5 : NoZeroSMulDivisors R M],
1 < FiniteDimensional.finrank R M → ∀ {x : M}, x ≠ 0 → ∃ y, LinearIndependent R ![x, y]
This theorem states that for any given nonzero vector in a finite-dimensional space where the dimension is greater than 1, there exists another vector that is linearly independent of the first one. This is applicable for a vector space `M` over a ring `R` that satisfies the rank-nullity theorem, the strong rank condition, and there are no zero scalar multiplications. The dimension of the vector space is described by the function `FiniteDimensional.finrank R M`. The linear independence of vectors is described by the predicate `LinearIndependent R ![x, y]` where `x` is the given nonzero vector and `y` is the vector that we claim to exist.
More concisely: Given a finite-dimensional vector space over a ring satisfying certain conditions, every nonzero vector has a linearly independent partner.
|
exists_linearIndependent_cons_of_lt_finrank
theorem exists_linearIndependent_cons_of_lt_finrank :
∀ {R : Type u_1} {M : Type u} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : HasRankNullity.{u, u_1} R] [inst_4 : StrongRankCondition R] {n : ℕ} {v : Fin n → M},
LinearIndependent R v → n < FiniteDimensional.finrank R M → ∃ x, LinearIndependent R (Fin.cons x v)
This theorem states that given a family of `n` linearly independent vectors in a finite-dimensional space of dimension `> n` over a ring `R`, we can always extend this family by adding another vector while preserving the property of linear independence. Specifically, if we have a module `M` over `R` with finite rank and a family `v` of `n` linearly independent vectors, where `n` is less than the rank of `M`, then there exists a vector `x` such that a new family formed by adding `x` to the start of `v` is still linearly independent.
More concisely: Given a module M over a ring R with finite rank and a family v of n linearly independent vectors in M (where n < rank(M)), there exists a linearly independent vector x such that [v, x] is also linearly independent.
|
exists_linearIndependent_pair_of_one_lt_rank
theorem exists_linearIndependent_pair_of_one_lt_rank :
∀ {R : Type u_1} {M : Type u} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : HasRankNullity.{u, u_1} R] [inst_4 : StrongRankCondition R] [inst_5 : NoZeroSMulDivisors R M],
1 < Module.rank R M → ∀ {x : M}, x ≠ 0 → ∃ y, LinearIndependent R ![x, y]
This theorem states that given a nonzero vector in a vector space with dimension greater than one over a ring `R`, there exists another vector that is linearly independent of the first one. More specifically, for any nonzero vector `x` in the vector space `M`, if the rank of the module `M` over `R` is more than one, then there exists a vector `y` such that the set `{x, y}` forms a linearly independent set. This theorem holds under the conditions that `R` is a ring, `M` is an additive commutative group and also a module over `R`. The ring `R` satisfies the strong rank condition and no zero divisors exist in the scalar multiplication of `M` by `R`.
More concisely: Given a nonzero vector `x` in a rank-greater-than-one vector space `M` over a ring `R` without zero divisors, there exists a linearly independent vector `y` in `M`.
|