# mathlibdocumentation

linear_algebra.finite_dimensional

# Finite dimensional vector spaces #

Definition and basic properties of finite dimensional vector spaces, of their dimensions, and of linear maps on such spaces.

## Main definitions #

Assume `V` is a vector space over a field `K`. There are (at least) three equivalent definitions of finite-dimensionality of `V`:

• it admits a finite basis.
• it is finitely generated.
• it is noetherian, i.e., every subspace is finitely generated.

We introduce a typeclass `finite_dimensional K V` capturing this property. For ease of transfer of proof, it is defined using the second point of view, i.e., as `finite`. However, we prove that all these points of view are equivalent, with the following lemmas (in the namespace `finite_dimensional`):

• `fintype_basis_index` states that a finite-dimensional vector space has a finite basis
• `finite_dimensional.fin_basis` and `finite_dimensional.fin_basis_of_finrank_eq` are bases for finite dimensional vector spaces, where the index type is `fin`
• `of_fintype_basis` states that the existence of a basis indexed by a finite type implies finite-dimensionality
• `of_finite_basis` states that the existence of a basis indexed by a finite set implies finite-dimensionality
• `is_noetherian.iff_fg` states that the space is finite-dimensional if and only if it is noetherian

Also defined is `finrank`, the dimension of a finite dimensional space, returning a `nat`, as opposed to `module.rank`, which returns a `cardinal`. When the space has infinite dimension, its `finrank` is by convention set to `0`.

Preservation of finite-dimensionality and formulas for the dimension are given for

• submodules
• quotients (for the dimension of a quotient, see `finrank_quotient_add_finrank`)
• linear equivs, in `linear_equiv.finite_dimensional` and `linear_equiv.finrank_eq`
• image under a linear map (the rank-nullity formula is in `finrank_range_add_finrank_ker`)

Basic properties of linear maps of a finite-dimensional vector space are given. Notably, the equivalence of injectivity and surjectivity is proved in `linear_map.injective_iff_surjective`, and the equivalence between left-inverse and right-inverse in `linear_map.mul_eq_one_comm` and `linear_map.comp_eq_id_comm`.

## Implementation notes #

Most results are deduced from the corresponding results for the general dimension (as a cardinal), in `dimension.lean`. Not all results have been ported yet.

Much of this file could be generalised away from fields or division rings. You should not assume that there has been any effort to state lemmas as generally as possible.

One of the characterizations of finite-dimensionality is in terms of finite generation. This property is currently defined only for submodules, so we express it through the fact that the maximal submodule (which, as a set, coincides with the whole space) is finitely generated. This is not very convenient to use, although there are some helper functions. However, this becomes very convenient when speaking of submodules which are finite-dimensional, as this notion coincides with the fact that the submodule is finitely generated (as a submodule of the whole space). This equivalence is proved in `submodule.fg_iff_finite_dimensional`.

@[reducible]
def finite_dimensional (K : Type u_1) (V : Type u_2) [ V] :
Prop

`finite_dimensional` vector spaces are defined to be finite modules. Use `finite_dimensional.of_fintype_basis` to prove finite dimension from another definition.

Equations
theorem finite_dimensional.of_injective {K : Type u} {V : Type v} [ V] {V₂ : Type v'} [add_comm_group V₂] [ V₂] (f : V →ₗ[K] V₂) (w : function.injective f) [ V₂] :

If the codomain of an injective linear map is finite dimensional, the domain must be as well.

theorem finite_dimensional.of_surjective {K : Type u} {V : Type v} [ V] {V₂ : Type v'} [add_comm_group V₂] [ V₂] (f : V →ₗ[K] V₂) (w : function.surjective f) [ V] :

If the domain of a surjective linear map is finite dimensional, the codomain must be as well.

@[protected, instance]
def finite_dimensional.finite_dimensional_pi (K : Type u) {ι : Type u_1} [finite ι] :
(ι → K)
@[protected, instance]
def finite_dimensional.finite_dimensional_pi' (K : Type u) {ι : Type u_1} [finite ι] (M : ι → Type u_2) [Π (i : ι), add_comm_group (M i)] [Π (i : ι), (M i)] [I : ∀ (i : ι), (M i)] :
(Π (i : ι), M i)
noncomputable def finite_dimensional.fintype_of_fintype (K : Type u) (V : Type v) [ V] [fintype K] [ V] :

A finite dimensional vector space over a finite field is finite

Equations
theorem finite_dimensional.finite_of_finite (K : Type u) (V : Type v) [ V] [finite K] [ V] :
theorem finite_dimensional.of_fintype_basis {K : Type u} {V : Type v} [ V] {ι : Type w} [finite ι] (h : K V) :

If a vector space has a finite basis, then it is finite-dimensional.

noncomputable def finite_dimensional.fintype_basis_index {K : Type u} {V : Type v} [ V] {ι : Type u_1} [ V] (b : K V) :

If a vector space is `finite_dimensional`, all bases are indexed by a finite type

Equations
• = let _inst : := finite_dimensional.fintype_basis_index._proof_1 in
@[protected, instance]
noncomputable def finite_dimensional.basis.of_vector_space_index.fintype {K : Type u} {V : Type v} [ V] [ V] :

If a vector space is `finite_dimensional`, `basis.of_vector_space` is indexed by a finite type.

Equations
theorem finite_dimensional.of_finite_basis {K : Type u} {V : Type v} [ V] {ι : Type w} {s : set ι} (h : K V) (hs : s.finite) :

If a vector space has a basis indexed by elements of a finite set, then it is finite-dimensional.

@[protected, instance]
def finite_dimensional.finite_dimensional_submodule {K : Type u} {V : Type v} [ V] [ V] (S : V) :

A subspace of a finite-dimensional space is also finite-dimensional.

@[protected, instance]
def finite_dimensional.finite_dimensional_quotient {K : Type u} {V : Type v} [ V] [ V] (S : V) :
(V S)

A quotient of a finite-dimensional space is also finite-dimensional.

noncomputable def finite_dimensional.finrank (R : Type u_1) (V : Type u_2) [semiring R] [ V] :

The rank of a module as a natural number.

Defined by convention to be `0` if the space has infinite rank.

For a vector space `V` over a field `K`, this is the same as the finite dimension of `V` over `K`.

Equations
theorem finite_dimensional.finrank_eq_dim (K : Type u) (V : Type v) [ V] [ V] :
= V

In a finite-dimensional space, its dimension (seen as a cardinal) coincides with its `finrank`.

theorem finite_dimensional.finrank_eq_of_dim_eq {K : Type u} {V : Type v} [ V] {n : } (h : V = n) :
theorem finite_dimensional.finrank_of_infinite_dimensional {K : Type u_1} {V : Type u_2} [ V] (h : ¬) :
theorem finite_dimensional.finite_dimensional_of_finrank {K : Type u_1} {V : Type u_2} [ V] (h : 0 < ) :
theorem finite_dimensional.finite_dimensional_of_finrank_eq_succ {K : Type u_1} {V : Type u_2} [field K] [ V] {n : } (hn : = n.succ) :
theorem finite_dimensional.fact_finite_dimensional_of_finrank_eq_succ {K : Type u_1} {V : Type u_2} [field K] [ V] (n : ) [fact = n + 1)] :

We can infer `finite_dimensional K V` in the presence of `[fact (finrank K V = n + 1)]`. Declare this as a local instance where needed.

theorem finite_dimensional.finite_dimensional_iff_of_rank_eq_nsmul {K : Type u_1} {V W : Type u_2} [field K] [ V] [ W] {n : } (hn : n 0) (hVW : V = n W) :
theorem finite_dimensional.finrank_eq_card_basis {K : Type u} {V : Type v} [ V] {ι : Type w} [fintype ι] (h : K V) :

If a vector space has a finite basis, then its dimension is equal to the cardinality of the basis.

theorem finite_dimensional.finrank_eq_card_basis' {K : Type u} {V : Type v} [ V] [ V] {ι : Type w} (h : K V) :

If a vector space is finite-dimensional, then the cardinality of any basis is equal to its `finrank`.

theorem finite_dimensional.finrank_eq_card_finset_basis {K : Type u} {V : Type v} [ V] {ι : Type w} {b : finset ι} (h : K V) :

If a vector space has a finite basis, then its dimension is equal to the cardinality of the basis. This lemma uses a `finset` instead of indexed types.

noncomputable def finite_dimensional.fin_basis (K : Type u) (V : Type v) [ V] [ V] :
basis (fin K V

A finite dimensional vector space has a basis indexed by `fin (finrank K V)`.

Equations
• = have h : , from _,
noncomputable def finite_dimensional.fin_basis_of_finrank_eq (K : Type u) (V : Type v) [ V] [ V] {n : } (hn : = n) :
basis (fin n) K V

An `n`-dimensional vector space has a basis indexed by `fin n`.

Equations
noncomputable def finite_dimensional.basis_unique {K : Type u} {V : Type v} [ V] (ι : Type u_1) [unique ι] (h : = 1) :
K V

A module with dimension 1 has a basis with one element.

Equations
@[simp]
theorem finite_dimensional.basis_unique.repr_eq_zero_iff {K : Type u} {V : Type v} [ V] {ι : Type u_1} [unique ι] {h : = 1} {v : V} {i : ι} :
(.repr) v) i = 0 v = 0
theorem finite_dimensional.cardinal_mk_le_finrank_of_linear_independent {K : Type u} {V : Type v} [ V] [ V] {ι : Type w} {b : ι → V} (h : b) :
theorem finite_dimensional.fintype_card_le_finrank_of_linear_independent {K : Type u} {V : Type v} [ V] [ V] {ι : Type u_1} [fintype ι] {b : ι → V} (h : b) :
theorem finite_dimensional.finset_card_le_finrank_of_linear_independent {K : Type u} {V : Type v} [ V] [ V] {b : finset V} (h : (λ (x : b), x)) :
theorem finite_dimensional.lt_aleph_0_of_linear_independent {K : Type u} {V : Type v} [ V] {ι : Type w} [ V] {v : ι → V} (h : v) :
theorem linear_independent.finite {K : Type u_1} {V : Type u_2} [ V] [ V] {b : set V} (h : (λ (x : b), x)) :
theorem finite_dimensional.not_linear_independent_of_infinite {K : Type u} {V : Type v} [ V] {ι : Type w} [inf : infinite ι] [ V] (v : ι → V) :
theorem finite_dimensional.finrank_pos_iff_exists_ne_zero {K : Type u} {V : Type v} [ V] [ V] :
∃ (x : V), x 0

A finite dimensional space has positive `finrank` iff it has a nonzero element.

theorem finite_dimensional.finrank_pos_iff {K : Type u} {V : Type v} [ V] [ V] :

A finite dimensional space has positive `finrank` iff it is nontrivial.

theorem finite_dimensional.nontrivial_of_finrank_pos {K : Type u} {V : Type v} [ V] (h : 0 < ) :

A finite dimensional space is nontrivial if it has positive `finrank`.

theorem finite_dimensional.nontrivial_of_finrank_eq_succ {K : Type u} {V : Type v} [ V] {n : } (hn : = n.succ) :

A finite dimensional space is nontrivial if it has `finrank` equal to the successor of a natural number.

theorem finite_dimensional.finrank_pos {K : Type u} {V : Type v} [ V] [ V] [h : nontrivial V] :

A nontrivial finite dimensional space has positive `finrank`.

theorem finite_dimensional.finrank_zero_iff {K : Type u} {V : Type v} [ V] [ V] :

A finite dimensional space has zero `finrank` iff it is a subsingleton. This is the `finrank` version of `dim_zero_iff`.

theorem finite_dimensional.finrank_zero_of_subsingleton {K : Type u} {V : Type v} [ V] [h : subsingleton V] :

A finite dimensional space that is a subsingleton has zero `finrank`.

theorem finite_dimensional.basis.subset_extend {K : Type u} {V : Type v} [ V] {s : set V} (hs : coe) :
s hs.extend _
theorem finite_dimensional.eq_top_of_finrank_eq {K : Type u} {V : Type v} [ V] [ V] {S : V}  :
S =

If a submodule has maximal dimension in a finite dimensional space, then it is equal to the whole space.

@[simp]
theorem finite_dimensional.finrank_self (K : Type u)  :

A division_ring is one-dimensional as a vector space over itself.

@[protected, instance]
@[simp]
theorem finite_dimensional.finrank_fintype_fun_eq_card (K : Type u) {ι : Type v} [fintype ι] :
(ι → K) =

The vector space of functions on a fintype ι has finrank equal to the cardinality of ι.

@[simp]
theorem finite_dimensional.finrank_fin_fun (K : Type u) {n : } :
(fin n → K) = n

The vector space of functions on `fin n` has finrank equal to `n`.

theorem finite_dimensional.span_of_finite (K : Type u) {V : Type v} [ V] {A : set V} (hA : A.finite) :

The submodule generated by a finite set is finite-dimensional.

@[protected, instance]
def finite_dimensional.span_singleton (K : Type u) {V : Type v} [ V] (x : V) :
{x})

The submodule generated by a single element is finite-dimensional.

@[protected, instance]
def finite_dimensional.span_finset (K : Type u) {V : Type v} [ V] (s : finset V) :

The submodule generated by a finset is finite-dimensional.

@[protected, instance]
def finite_dimensional.submodule.map.finite_dimensional (K : Type u) {V : Type v} [ V] {V₂ : Type v'} [add_comm_group V₂] [ V₂] (f : V →ₗ[K] V₂) (p : V) [h : p] :
p)

Pushforwards of finite-dimensional submodules are finite-dimensional.

theorem finite_dimensional.finrank_map_le (K : Type u) {V : Type v} [ V] {V₂ : Type v'} [add_comm_group V₂] [ V₂] (f : V →ₗ[K] V₂) (p : V) [ p] :

Pushforwards of finite-dimensional submodules have a smaller finrank.

theorem complete_lattice.independent.subtype_ne_bot_le_finrank_aux {K : Type u} {V : Type v} [ V] [ V] {ι : Type w} {p : ι → V} (hp : complete_lattice.independent p) :
cardinal.mk {i // p i }
noncomputable def complete_lattice.independent.fintype_ne_bot_of_finite_dimensional {K : Type u} {V : Type v} [ V] [ V] {ι : Type w} {p : ι → V} (hp : complete_lattice.independent p) :
fintype {i // p i }

If `p` is an independent family of subspaces of a finite-dimensional space `V`, then the number of nontrivial subspaces in the family `p` is finite.

Equations
theorem complete_lattice.independent.subtype_ne_bot_le_finrank {K : Type u} {V : Type v} [ V] [ V] {ι : Type w} {p : ι → V} (hp : complete_lattice.independent p) [fintype {i // p i }] :
fintype.card {i // p i }

If `p` is an independent family of subspaces of a finite-dimensional space `V`, then the number of nontrivial subspaces in the family `p` is bounded above by the dimension of `V`.

Note that the `fintype` hypothesis required here can be provided by `complete_lattice.independent.fintype_ne_bot_of_finite_dimensional`.

theorem finite_dimensional.exists_nontrivial_relation_of_dim_lt_card {K : Type u} {V : Type v} [ V] [ V] {t : finset V} (h : < t.card) :
∃ (f : V → K), t.sum (λ (e : V), f e e) = 0 ∃ (x : V) (H : x t), f x 0

If a finset has cardinality larger than the dimension of the space, then there is a nontrivial linear relation amongst its elements.

theorem finite_dimensional.exists_nontrivial_relation_sum_zero_of_dim_succ_lt_card {K : Type u} {V : Type v} [ V] [ V] {t : finset V} (h : < t.card) :
∃ (f : V → K), t.sum (λ (e : V), f e e) = 0 t.sum (λ (e : V), f e) = 0 ∃ (x : V) (H : x t), f x 0

If a finset has cardinality larger than `finrank + 1`, then there is a nontrivial linear relation amongst its elements, such that the coefficients of the relation sum to zero.

theorem finite_dimensional.exists_relation_sum_zero_pos_coefficient_of_dim_succ_lt_card {L : Type u_1} {W : Type v} [ W] [ W] {t : finset W} (h : < t.card) :
∃ (f : W → L), t.sum (λ (e : W), f e e) = 0 t.sum (λ (e : W), f e) = 0 ∃ (x : W) (H : x t), 0 < f x

A slight strengthening of `exists_nontrivial_relation_sum_zero_of_dim_succ_lt_card` available when working over an ordered field: we can ensure a positive coefficient, not just a nonzero coefficient.

@[simp]
theorem finite_dimensional.basis_singleton_repr_apply {K : Type u} {V : Type v} [ V] (ι : Type u_1) [unique ι] (h : = 1) (v : V) (hv : v 0) (w : V) :
hv).repr) w =
@[simp]
theorem finite_dimensional.basis_singleton_repr_symm_apply {K : Type u} {V : Type v} [ V] (ι : Type u_1) [unique ι] (h : = 1) (v : V) (hv : v 0) (f : ι →₀ K) :
hv).repr.symm) f =
noncomputable def finite_dimensional.basis_singleton {K : Type u} {V : Type v} [ V] (ι : Type u_1) [unique ι] (h : = 1) (v : V) (hv : v 0) :
K V

In a vector space with dimension 1, each set {v} is a basis for `v ≠ 0`.

Equations
@[simp]
theorem finite_dimensional.basis_singleton_apply {K : Type u} {V : Type v} [ V] (ι : Type u_1) [unique ι] (h : = 1) (v : V) (hv : v 0) (i : ι) :
hv) i = v
@[simp]
theorem finite_dimensional.range_basis_singleton {K : Type u} {V : Type v} [ V] (ι : Type u_1) [unique ι] (h : = 1) (v : V) (hv : v 0) :
set.range hv) = {v}
theorem finite_dimensional_of_dim_eq_zero {K : Type u} {V : Type v} [ V] (h : V = 0) :
theorem finite_dimensional_of_dim_eq_one {K : Type u} {V : Type v} [ V] (h : V = 1) :
theorem finrank_eq_zero_of_dim_eq_zero {K : Type u} {V : Type v} [ V] [ V] (h : V = 0) :
theorem finrank_eq_zero_of_basis_imp_not_finite {K : Type u} {V : Type v} [ V] (h : ∀ (s : set V), K V¬s.finite) :
theorem finrank_eq_zero_of_basis_imp_false {K : Type u} {V : Type v} [ V] (h : ∀ (s : finset V), K Vfalse) :
theorem finrank_eq_zero_of_not_exists_basis {K : Type u} {V : Type v} [ V] (h : ¬∃ (s : finset V), nonempty (basis s K V)) :
theorem finrank_eq_zero_of_not_exists_basis_finite {K : Type u} {V : Type v} [ V] (h : ¬∃ (s : set V) (b : K V), s.finite) :
theorem finrank_eq_zero_of_not_exists_basis_finset {K : Type u} {V : Type v} [ V] (h : ¬∃ (s : finset V), nonempty (basis s K V)) :
@[protected, instance]
def finite_dimensional_bot (K : Type u) (V : Type v) [ V] :
@[simp]
theorem finrank_bot (K : Type u) (V : Type v) [ V] :
theorem bot_eq_top_of_dim_eq_zero {K : Type u} {V : Type v} [ V] (h : V = 0) :
@[simp]
theorem dim_eq_zero {K : Type u} {V : Type v} [ V] {S : V} :
S = 0 S =
@[simp]
theorem finrank_eq_zero {K : Type u} {V : Type v} [ V] {S : V} [ S] :
S =
theorem submodule.fg_iff_finite_dimensional {K : Type u} {V : Type v} [ V] (s : V) :
s.fg

A submodule is finitely generated if and only if it is finite-dimensional

theorem submodule.finite_dimensional_of_le {K : Type u} {V : Type v} [ V] {S₁ S₂ : V} [ S₂] (h : S₁ S₂) :

A submodule contained in a finite-dimensional submodule is finite-dimensional.

@[protected, instance]
def submodule.finite_dimensional_inf_left {K : Type u} {V : Type v} [ V] (S₁ S₂ : V) [ S₁] :
(S₁ S₂)

The inf of two submodules, the first finite-dimensional, is finite-dimensional.

@[protected, instance]
def submodule.finite_dimensional_inf_right {K : Type u} {V : Type v} [ V] (S₁ S₂ : V) [ S₂] :
(S₁ S₂)

The inf of two submodules, the second finite-dimensional, is finite-dimensional.

@[protected, instance]
def submodule.finite_dimensional_sup {K : Type u} {V : Type v} [ V] (S₁ S₂ : V) [h₁ : S₁] [h₂ : S₂] :
(S₁ S₂)

The sup of two finite-dimensional submodules is finite-dimensional.

@[protected, instance]
def submodule.finite_dimensional_finset_sup {K : Type u} {V : Type v} [ V] {ι : Type u_1} (s : finset ι) (S : ι → V) [∀ (i : ι), (S i)] :
(s.sup S)

The submodule generated by a finite supremum of finite dimensional submodules is finite-dimensional.

Note that strictly this only needs `∀ i ∈ s, finite_dimensional K (S i)`, but that doesn't work well with typeclass search.

@[protected, instance]
def submodule.finite_dimensional_supr {K : Type u} {V : Type v} [ V] {ι : Type u_1} [finite ι] (S : ι → V) [∀ (i : ι), (S i)] :
(⨆ (i : ι), S i)

The submodule generated by a supremum of finite dimensional submodules, indexed by a finite type is finite-dimensional.

@[protected, instance]
def submodule.finite_dimensional_supr_prop {K : Type u} {V : Type v} [ V] {P : Prop} (S : P → V) [∀ (h : P), (S h)] :
(⨆ (h : P), S h)

The submodule generated by a supremum indexed by a proposition is finite-dimensional if the submodule is.

theorem submodule.finrank_le {K : Type u} {V : Type v} [ V] [ V] (s : V) :

The dimension of a submodule is bounded by the dimension of the ambient space.

theorem submodule.finrank_quotient_le {K : Type u} {V : Type v} [ V] [ V] (s : V) :

The dimension of a quotient is bounded by the dimension of the ambient space.

theorem submodule.finrank_quotient_add_finrank {K : Type u} {V : Type v} [field K] [ V] [ V] (s : V) :

In a finite-dimensional vector space, the dimensions of a submodule and of the corresponding quotient add up to the dimension of the space.

theorem submodule.finrank_lt {K : Type u} {V : Type v} [field K] [ V] [ V] {s : V} (h : s < ) :

The dimension of a strict submodule is strictly bounded by the dimension of the ambient space.

theorem submodule.dim_sup_add_dim_inf_eq {K : Type u} {V : Type v} [field K] [ V] (s t : V) [ s] [ t] :
(s t) + (s t) =

The sum of the dimensions of s + t and s ∩ t is the sum of the dimensions of s and t

theorem submodule.dim_add_le_dim_add_dim {K : Type u} {V : Type v} [field K] [ V] (s t : V) [ s] [ t] :
theorem submodule.eq_top_of_disjoint {K : Type u} {V : Type v} [field K] [ V] [ V] (s t : V) (hdim : = ) (hdisjoint : t) :
s t =
@[protected]
theorem linear_equiv.finite_dimensional {K : Type u} {V : Type v} [ V] {V₂ : Type v'} [add_comm_group V₂] [ V₂] (f : V ≃ₗ[K] V₂) [ V] :

Finite dimensionality is preserved under linear equivalence.

theorem linear_equiv.finrank_eq {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [ring R] [add_comm_group M₂] [ M] [ M₂] (f : M ≃ₗ[R] M₂) :

The dimension of a finite dimensional space is preserved under linear equivalence.

theorem linear_equiv.finrank_map_eq {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [ring R] [add_comm_group M₂] [ M] [ M₂] (f : M ≃ₗ[R] M₂) (p : M) :

Pushforwards of finite-dimensional submodules along a `linear_equiv` have the same finrank.

@[protected, instance]
def finite_dimensional_finsupp {K : Type u} {V : Type v} [ V] {ι : Type u_1} [finite ι] [h : V] :
→₀ V)
theorem finite_dimensional.nonempty_linear_equiv_of_finrank_eq {K : Type u} {V : Type v} [ V] {V₂ : Type v'} [add_comm_group V₂] [ V₂] [ V] [ V₂] (cond : = ) :
nonempty (V ≃ₗ[K] V₂)

Two finite-dimensional vector spaces are isomorphic if they have the same (finite) dimension.

theorem finite_dimensional.nonempty_linear_equiv_iff_finrank_eq {K : Type u} {V : Type v} [ V] {V₂ : Type v'} [add_comm_group V₂] [ V₂] [ V] [ V₂] :
nonempty (V ≃ₗ[K] V₂)

Two finite-dimensional vector spaces are isomorphic if and only if they have the same (finite) dimension.

noncomputable def finite_dimensional.linear_equiv.of_finrank_eq {K : Type u} (V : Type v) [ V] (V₂ : Type v') [add_comm_group V₂] [ V₂] [ V] [ V₂] (cond : = ) :
V ≃ₗ[K] V₂

Two finite-dimensional vector spaces are isomorphic if they have the same (finite) dimension.

Equations
theorem finite_dimensional.eq_of_le_of_finrank_le {K : Type u} {V : Type v} [ V] {S₁ S₂ : V} [ S₂] (hle : S₁ S₂) (hd : ) :
S₁ = S₂
theorem finite_dimensional.eq_of_le_of_finrank_eq {K : Type u} {V : Type v} [ V] {S₁ S₂ : V} [ S₂] (hle : S₁ S₂) (hd : = ) :
S₁ = S₂

If a submodule is less than or equal to a finite-dimensional submodule with the same dimension, they are equal.

@[simp]
theorem finite_dimensional.finrank_map_subtype_eq {K : Type u} {V : Type v} [ V] (p : V) (q : p) :
noncomputable def finite_dimensional.linear_equiv.quot_equiv_of_equiv {K : Type u} {V : Type v} [field K] [ V] {V₂ : Type v'} [add_comm_group V₂] [ V₂] [ V] [ V₂] {p : V} {q : V₂} (f₁ : p ≃ₗ[K] q) (f₂ : V ≃ₗ[K] V₂) :
(V p) ≃ₗ[K] V₂ q

Given isomorphic subspaces `p q` of vector spaces `V` and `V₁` respectively, `p.quotient` is isomorphic to `q.quotient`.

Equations
noncomputable def finite_dimensional.linear_equiv.quot_equiv_of_quot_equiv {K : Type u} {V : Type v} [field K] [ V] [ V] {p q : V} (f : (V p) ≃ₗ[K] q) :
(V q) ≃ₗ[K] p

Given the subspaces `p q`, if `p.quotient ≃ₗ[K] q`, then `q.quotient ≃ₗ[K] p`

Equations
theorem linear_map.surjective_of_injective {K : Type u} {V : Type v} [ V] [ V] {f : V →ₗ[K] V} (hinj : function.injective f) :

On a finite-dimensional space, an injective linear map is surjective.

theorem linear_map.finite_dimensional_of_surjective {K : Type u} {V : Type v} [ V] {V₂ : Type v'} [add_comm_group V₂] [ V₂] [h : V] (f : V →ₗ[K] V₂) (hf : = ) :

The image under an onto linear map of a finite-dimensional space is also finite-dimensional.

@[protected, instance]
def linear_map.finite_dimensional_range {K : Type u} {V : Type v} [ V] {V₂ : Type v'} [add_comm_group V₂] [ V₂] [h : V] (f : V →ₗ[K] V₂) :

The range of a linear map defined on a finite-dimensional space is also finite-dimensional.

theorem linear_map.finrank_range_of_inj {K : Type u} {V : Type v} [ V] {V₂ : Type v'} [add_comm_group V₂] [ V₂] {f : V →ₗ[K] V₂} (hf : function.injective f) :

The dimensions of the domain and range of an injective linear map are equal.

theorem linear_map.injective_iff_surjective {K : Type u} {V : Type v} [field K] [ V] [ V] {f : V →ₗ[K] V} :

On a finite-dimensional space, a linear map is injective if and only if it is surjective.

theorem linear_map.ker_eq_bot_iff_range_eq_top {K : Type u} {V : Type v} [field K] [ V] [ V] {f : V →ₗ[K] V} :
theorem linear_map.mul_eq_one_of_mul_eq_one {K : Type u} {V : Type v} [field K] [ V] [ V] {f g : V →ₗ[K] V} (hfg : f * g = 1) :
g * f = 1

In a finite-dimensional space, if linear maps are inverse to each other on one side then they are also inverse to each other on the other side.

theorem linear_map.mul_eq_one_comm {K : Type u} {V : Type v} [field K] [ V] [ V] {f g : V →ₗ[K] V} :
f * g = 1 g * f = 1

In a finite-dimensional space, linear maps are inverse to each other on one side if and only if they are inverse to each other on the other side.

theorem linear_map.comp_eq_id_comm {K : Type u} {V : Type v} [field K] [ V] [ V] {f g : V →ₗ[K] V} :

In a finite-dimensional space, linear maps are inverse to each other on one side if and only if they are inverse to each other on the other side.

theorem linear_map.finrank_range_add_finrank_ker {K : Type u} {V : Type v} [field K] [ V] {V₂ : Type v'} [add_comm_group V₂] [ V₂] [ V] (f : V →ₗ[K] V₂) :

rank-nullity theorem : the dimensions of the kernel and the range of a linear map add up to the dimension of the source space.

noncomputable def linear_equiv.of_injective_endo {K : Type u} {V : Type v} [field K] [ V] [ V] (f : V →ₗ[K] V) (h_inj : function.injective f) :

The linear equivalence corresponging to an injective endomorphism.

Equations
• = h_inj _
@[simp]
theorem linear_equiv.coe_of_injective_endo {K : Type u} {V : Type v} [field K] [ V] [ V] (f : V →ₗ[K] V) (h_inj : function.injective f) :
h_inj) = f
@[simp]
theorem linear_equiv.of_injective_endo_right_inv {K : Type u} {V : Type v} [field K] [ V] [ V] (f : V →ₗ[K] V) (h_inj : function.injective f) :
f * h_inj).symm) = 1
@[simp]
theorem linear_equiv.of_injective_endo_left_inv {K : Type u} {V : Type v} [field K] [ V] [ V] (f : V →ₗ[K] V) (h_inj : function.injective f) :
h_inj).symm) * f = 1
theorem linear_map.is_unit_iff_ker_eq_bot {K : Type u} {V : Type v} [field K] [ V] [ V] (f : V →ₗ[K] V) :
theorem linear_map.is_unit_iff_range_eq_top {K : Type u} {V : Type v} [field K] [ V] [ V] (f : V →ₗ[K] V) :
@[simp]
theorem finrank_top {K : Type u} {V : Type v} [ V] :
theorem finrank_zero_iff_forall_zero {K : Type u} {V : Type v} [ V] [ V] :
∀ (x : V), x = 0
noncomputable def basis_of_finrank_zero {K : Type u} {V : Type v} [ V] [ V] {ι : Type u_1} [is_empty ι] (hV : = 0) :
K V

If `ι` is an empty type and `V` is zero-dimensional, there is a unique `ι`-indexed basis.

Equations
theorem linear_map.injective_iff_surjective_of_finrank_eq_finrank {K : Type u} {V : Type v} [field K] [ V] {V₂ : Type v'} [add_comm_group V₂] [ V₂] [ V] [ V₂] (H : = ) {f : V →ₗ[K] V₂} :
theorem linear_map.ker_eq_bot_iff_range_eq_top_of_finrank_eq_finrank {K : Type u} {V : Type v} [field K] [ V] {V₂ : Type v'} [add_comm_group V₂] [ V₂] [ V] [ V₂] (H : = ) {f : V →ₗ[K] V₂} :
theorem linear_map.finrank_le_finrank_of_injective {K : Type u} {V : Type v} [field K] [ V] {V₂ : Type v'} [add_comm_group V₂] [ V₂] [ V] [ V₂] {f : V →ₗ[K] V₂} (hf : function.injective f) :
noncomputable def linear_map.linear_equiv_of_injective {K : Type u} {V : Type v} [field K] [ V] {V₂ : Type v'} [add_comm_group V₂] [ V₂] [ V] [ V₂] (f : V →ₗ[K] V₂) (hf : function.injective f) (hdim : = ) :
V ≃ₗ[K] V₂

Given a linear map `f` between two vector spaces with the same dimension, if `ker f = ⊥` then `linear_equiv_of_injective` is the induced isomorphism between the two vector spaces.

Equations
• hdim =
@[simp]
theorem linear_map.linear_equiv_of_injective_apply {K : Type u} {V : Type v} [field K] [ V] {V₂ : Type v'} [add_comm_group V₂] [ V₂] [ V] [ V₂] {f : V →ₗ[K] V₂} (hf : function.injective f) (hdim : = ) (x : V) :
hdim) x = f x
noncomputable def division_ring_of_finite_dimensional (F : Type u_1) (K : Type u_2) [field F] [ring K] [is_domain K] [ K] [ K] :

A domain that is module-finite as an algebra over a field is a division ring.

Equations
noncomputable def field_of_finite_dimensional (F : Type u_1) (K : Type u_2) [field F] [comm_ring K] [is_domain K] [ K] [ K] :

An integral domain that is module-finite as an algebra over a field is a field.

Equations
theorem submodule.lt_of_le_of_finrank_lt_finrank {K : Type u} {V : Type v} [ V] {s t : V} (le : s t) (lt : < ) :
s < t
theorem submodule.lt_top_of_finrank_lt_finrank {K : Type u} {V : Type v} [ V] {s : V} (lt : < ) :
s <
theorem submodule.finrank_mono {K : Type u} {V : Type v} [ V] [ V] :
monotone (λ (s : V),
theorem submodule.finrank_lt_finrank_of_lt {K : Type u} {V : Type v} [field K] [ V] [ V] {s t : V} (hst : s < t) :
theorem submodule.finrank_add_eq_of_is_compl {K : Type u} {V : Type v} [field K] [ V] [ V] {U W : V} (h : W) :
@[protected]
noncomputable def set.finrank (K : Type u) {V : Type v} [ V] (s : set V) :

The rank of a set of vectors as a natural number.

Equations
theorem finrank_span_le_card {K : Type u} {V : Type v} [ V] (s : set V) [fintype s] :
theorem finrank_span_finset_le_card {K : Type u} {V : Type v} [ V] (s : finset V) :
theorem finrank_range_le_card {K : Type u} {V : Type v} [ V] {ι : Type u_1} [fintype ι] {b : ι → V} :
theorem finrank_span_eq_card {K : Type u} {V : Type v} [ V] {ι : Type u_1} [fintype ι] {b : ι → V} (hb : b) :
theorem finrank_span_set_eq_card {K : Type u} {V : Type v} [ V] (s : set V) [fintype s] (hs : coe) :
theorem finrank_span_finset_eq_card {K : Type u} {V : Type v} [ V] (s : finset V) (hs : coe) :
theorem span_lt_of_subset_of_card_lt_finrank {K : Type u} {V : Type v} [ V] {s : set V} [fintype s] {t : V} (subset : s t) (card_lt : s.to_finset.card < ) :
< t
theorem span_lt_top_of_card_lt_finrank {K : Type u} {V : Type v} [ V] {s : set V} [fintype s] (card_lt : s.to_finset.card < ) :
theorem finrank_span_singleton {K : Type u} {V : Type v} [ V] {v : V} (hv : v 0) :
= 1
theorem set.finrank_mono {K : Type u} {V : Type v} [field K] [ V] [ V] {s t : set V} (h : s t) :
s t
theorem linear_independent_of_top_le_span_of_card_eq_finrank {K : Type u} {V : Type v} [ V] {ι : Type u_1} [fintype ι] {b : ι → V} (spans : (set.range b)) (card_eq : = ) :
theorem linear_independent_iff_card_eq_finrank_span {K : Type u} {V : Type v} [ V] {ι : Type u_1} [fintype ι] {b : ι → V} :

A finite family of vectors is linearly independent if and only if its cardinality equals the dimension of its span.

theorem linear_independent_iff_card_le_finrank_span {K : Type u} {V : Type v} [ V] {ι : Type u_1} [fintype ι] {b : ι → V} :
noncomputable def basis_of_top_le_span_of_card_eq_finrank {K : Type u} {V : Type v} [ V] {ι : Type u_1} [fintype ι] (b : ι → V) (le_span : (set.range b)) (card_eq : = ) :
K V

A family of `finrank K V` vectors forms a basis if they span the whole space.

Equations
• card_eq = le_span
@[simp]
theorem coe_basis_of_top_le_span_of_card_eq_finrank {K : Type u} {V : Type v} [ V] {ι : Type u_1} [fintype ι] (b : ι → V) (le_span : (set.range b)) (card_eq : = ) :
le_span card_eq) = b
@[simp]
theorem finset_basis_of_top_le_span_of_card_eq_finrank_repr_symm_apply {K : Type u} {V : Type v} [ V] {s : finset V} (le_span : ) (card_eq : s.card = ) (ᾰ : s →₀ K) :
card_eq).repr.symm) = V K coe)
noncomputable def finset_basis_of_top_le_span_of_card_eq_finrank {K : Type u} {V : Type v} [ V] {s : finset V} (le_span : ) (card_eq : s.card = ) :
K V

A finset of `finrank K V` vectors forms a basis if they span the whole space.

Equations
@[simp]
theorem finset_basis_of_top_le_span_of_card_eq_finrank_repr_apply {K : Type u} {V : Type v} [ V] {s : finset V} (le_span : ) (card_eq : s.card = ) (ᾰ : V) :
card_eq).repr) = (_.repr) ᾰ)
@[simp]
theorem set_basis_of_top_le_span_of_card_eq_finrank_repr_symm_apply {K : Type u} {V : Type v} [ V] {s : set V} [fintype s] (le_span : ) (card_eq : s.to_finset.card = ) (ᾰ : s →₀ K) :
card_eq).repr.symm) = V K coe)
@[simp]
theorem set_basis_of_top_le_span_of_card_eq_finrank_repr_apply {K : Type u} {V : Type v} [ V] {s : set V} [fintype s] (le_span : ) (card_eq : s.to_finset.card = ) (ᾰ : V) :
card_eq).repr) = (_.repr) ᾰ)
noncomputable def set_basis_of_top_le_span_of_card_eq_finrank {K : Type u} {V : Type v} [ V] {s : set V} [fintype s] (le_span : ) (card_eq : s.to_finset.card = ) :
K V

A set of `finrank K V` vectors forms a basis if they span the whole space.

Equations
theorem span_eq_top_of_linear_independent_of_card_eq_finrank {K : Type u} {V : Type v} [field K] [ V] {ι : Type u_1} [hι : nonempty ι] [fintype ι] {b : ι → V} (lin_ind : b) (card_eq : = ) :
noncomputable def basis_of_linear_independent_of_card_eq_finrank {K : Type u} {V : Type v} [field K] [ V] {ι : Type u_1} [nonempty ι] [fintype ι] {b : ι → V} (lin_ind : b) (card_eq : = ) :
K V

A linear independent family of `finrank K V` vectors forms a basis.

Equations
@[simp]
theorem basis_of_linear_independent_of_card_eq_finrank_repr_apply {K : Type u} {V : Type v} [field K] [ V] {ι : Type u_1} [nonempty ι] [fintype ι] {b : ι → V} (lin_ind : b) (card_eq : = ) (ᾰ : V) :
card_eq).repr) = (lin_ind.repr) ( ᾰ)
@[simp]
theorem basis_of_linear_independent_of_card_eq_finrank_repr_symm_apply {K : Type u} {V : Type v} [field K] [ V] {ι : Type u_1} [nonempty ι] [fintype ι] {b : ι → V} (lin_ind : b) (card_eq : = ) (ᾰ : ι →₀ K) :
card_eq).repr.symm) = V K b)
@[simp]
theorem coe_basis_of_linear_independent_of_card_eq_finrank {K : Type u} {V : Type v} [field K] [ V] {ι : Type u_1} [nonempty ι] [fintype ι] {b : ι → V} (lin_ind : b) (card_eq : = ) :
card_eq) = b
@[simp]
theorem finset_basis_of_linear_independent_of_card_eq_finrank_repr_symm_apply {K : Type u} {V : Type v} [field K] [ V] {s : finset V} (hs : s.nonempty) (lin_ind : coe) (card_eq : s.card = ) (ᾰ : {x // x s} →₀ K) :
card_eq).repr.symm) = (finsupp.total {x // x s} V K coe)
@[simp]
theorem finset_basis_of_linear_independent_of_card_eq_finrank_repr_apply {K : Type u} {V : Type v} [field K] [ V] {s : finset V} (hs : s.nonempty) (lin_ind : coe) (card_eq : s.card = ) (ᾰ : V) :
card_eq).repr) = (lin_ind.repr) ᾰ)
noncomputable def finset_basis_of_linear_independent_of_card_eq_finrank {K : Type u} {V : Type v} [field K] [ V] {s : finset V} (hs : s.nonempty) (lin_ind : coe) (card_eq : s.card = ) :
K V

A linear independent finset of `finrank K V` vectors forms a basis.

Equations
• card_eq =
@[simp]
theorem coe_finset_basis_of_linear_independent_of_card_eq_finrank {K : Type u} {V : Type v} [field K] [ V] {s : finset V} (hs : s.nonempty) (lin_ind : coe) (card_eq : s.card = ) :
card_eq) = coe
noncomputable def set_basis_of_linear_independent_of_card_eq_finrank {K : Type u} {V : Type v} [field K] [ V] {s : set V} [nonempty s] [fintype s] (lin_ind : coe) (card_eq : s.to_finset.card = ) :
K V

A linear independent set of `finrank K V` vectors forms a basis.

Equations
• card_eq =
@[simp]
theorem set_basis_of_linear_independent_of_card_eq_finrank_repr_symm_apply {K : Type u} {V : Type v} [field K] [ V] {s : set V} [nonempty s] [fintype s] (lin_ind : coe) (card_eq : s.to_finset.card = ) (ᾰ : s →₀ K) :
card_eq).repr.symm) = V K coe)
@[simp]
theorem set_basis_of_linear_independent_of_card_eq_finrank_repr_apply {K : Type u} {V : Type v} [field K] [ V] {s : set V} [nonempty s] [fintype s] (lin_ind : coe) (card_eq : s.to_finset.card = ) (ᾰ : V) :
card_eq).repr) = (lin_ind.repr) ᾰ)
@[simp]
theorem coe_set_basis_of_linear_independent_of_card_eq_finrank {K : Type u} {V : Type v} [field K] [ V] {s : set V} [nonempty s] [fintype s] (lin_ind : coe) (card_eq : s.to_finset.card = ) :
card_eq) = coe

We now give characterisations of `finrank K V = 1` and `finrank K V ≤ 1`.

theorem finrank_eq_one {K : Type u} {V : Type v} [ V] (v : V) (n : v 0) (h : ∀ (w : V), ∃ (c : K), c v = w) :

If there is a nonzero vector and every other vector is a multiple of it, then the module has dimension one.

theorem finrank_le_one {K : Type u} {V : Type v} [ V] (v : V) (h : ∀ (w : V), ∃ (c : K), c v = w) :

If every vector is a multiple of some `v : V`, then `V` has dimension at most one.

theorem finrank_eq_one_iff_of_nonzero {K : Type u} {V : Type v} [ V] (v : V) (nz : v 0) :
{v} =

A vector space with a nonzero vector `v` has dimension 1 iff `v` spans.

theorem finrank_eq_one_iff_of_nonzero' {K : Type u} {V : Type v} [ V] (v : V) (nz : v 0) :
∀ (w : V), ∃ (c : K), c v = w

A module with a nonzero vector `v` has dimension 1 iff every vector is a multiple of `v`.

theorem finrank_eq_one_iff {K : Type u} {V : Type v} [ V] (ι : Type u_1) [unique ι] :
nonempty (basis ι K V)

A module has dimension 1 iff there is some `v : V` so `{v}` is a basis.

theorem finrank_eq_one_iff' {K : Type u} {V : Type v} [ V] :
∃ (v : V) (n : v 0), ∀ (w : V), ∃ (c : K), c v = w

A module has dimension 1 iff there is some nonzero `v : V` so every vector is a multiple of `v`.

theorem finrank_le_one_iff {K : Type u} {V : Type v} [ V] [ V] :
∃ (v : V), ∀ (w : V), ∃ (c : K), c v = w

A finite dimensional module has dimension at most 1 iff there is some `v : V` so every vector is a multiple of `v`.

theorem submodule.finrank_le_one_iff_is_principal {K : Type u} {V : Type v} [ V] (W : V) [ W] :
theorem module.finrank_le_one_iff_top_is_principal {K : Type u} {V : Type v} [ V] [ V] :
theorem surjective_of_nonzero_of_finrank_eq_one {V : Type v} {K : Type u_1} {A : Type u_2} [semiring A] [ V] [ V] {W : Type u_3} [ W] [ W] [ A] (h : = 1) {f : V →ₗ[A] W} (w : f 0) :
theorem subalgebra.dim_eq_one_of_eq_bot {F : Type u_1} {E : Type u_2} [field F] [field E] [ E] {S : E} (h : S = ) :
S = 1
@[simp]
theorem subalgebra.dim_bot {F : Type u_1} {E : Type u_2} [field F] [field E] [ E] :
= 1
theorem subalgebra_top_dim_eq_submodule_top_dim {F : Type u_1} {E : Type u_2} [field F] [field E] [ E] :
theorem subalgebra_top_finrank_eq_submodule_top_finrank {F : Type u_1} {E : Type u_2} [field F] [field E] [ E] :
theorem subalgebra.dim_top {F : Type u_1} {E : Type u_2} [field F] [field E] [ E] :
= E
@[protected, instance]
def subalgebra.finite_dimensional_bot {F : Type u_1} {E : Type u_2} [field F] [field E] [ E] :
@[simp]
theorem subalgebra.finrank_bot {F : Type u_1} {E : Type u_2} [field F] [field E] [ E] :
theorem subalgebra.finrank_eq_one_of_eq_bot {F : Type u_1} {E : Type u_2} [field F] [field E] [ E] {S : E} (h : S = ) :
theorem subalgebra.eq_bot_of_finrank_one {F : Type u_1} {E : Type u_2} [field F] [field E] [ E] {S : E} (h : = 1) :
S =
theorem subalgebra.eq_bot_of_dim_one {F : Type u_1} {E : Type u_2} [field F] [field E] [ E] {S : E} (h : S = 1) :
S =
@[simp]
theorem subalgebra.bot_eq_top_of_dim_eq_one {F : Type u_1} {E : Type u_2} [field F] [field E] [ E] (h : E = 1) :
@[simp]
theorem subalgebra.bot_eq_top_of_finrank_eq_one {F : Type u_1} {E : Type u_2} [field F] [field E] [ E] (h : = 1) :
@[simp]
theorem subalgebra.dim_eq_one_iff {F : Type u_1} {E : Type u_2} [field F] [field E] [ E] {S : E} :
S = 1 S =
@[simp]
theorem subalgebra.finrank_eq_one_iff {F : Type u_1} {E : Type u_2} [field F] [field E] [ E] {S : E} :
S =
theorem module.End.exists_ker_pow_eq_ker_pow_succ {K : Type u} {V : Type v} [field K] [ V] [ V] (f : V) :
∃ (k : ), linear_map.ker (f ^ k) = linear_map.ker (f ^ k.succ)
theorem module.End.ker_pow_constant {K : Type u} {V : Type v} [field K] [ V] {f : V} {k : } (h : linear_map.ker (f ^ k) = linear_map.ker (f ^ k.succ)) (m : ) :
theorem module.End.ker_pow_eq_ker_pow_finrank_of_le {K : Type u} {V : Type v} [field K] [ V] [ V] {f : V} {m : } (hm : m) :
theorem module.End.ker_pow_le_ker_pow_finrank {K : Type u} {V : Type v} [field K] [ V] [ V] (f : V) (m : ) :