mathlib3 documentation

linear_algebra.finite_dimensional

Finite dimensional vector spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 division ring K. There are (at least) three equivalent definitions of finite-dimensionality of V:

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):

We make use of 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. finrank is not defined using finite_dimensional. For basic results that do not need the finite_dimensional class, import linear_algebra.finrank.

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

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.

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) [division_ring K] [add_comm_group V] [module K 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} [division_ring K] [add_comm_group V] [module K V] {V₂ : Type v'} [add_comm_group V₂] [module K V₂] (f : V →ₗ[K] V₂) (w : function.injective f) [finite_dimensional K 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} [division_ring K] [add_comm_group V] [module K V] {V₂ : Type v'} [add_comm_group V₂] [module K V₂] (f : V →ₗ[K] V₂) (w : function.surjective f) [finite_dimensional K V] :

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

@[protected, instance]
@[protected, instance]
def finite_dimensional.finite_dimensional_pi' (K : Type u) [division_ring K] {ι : Type u_1} [finite ι] (M : ι Type u_2) [Π (i : ι), add_comm_group (M i)] [Π (i : ι), module K (M i)] [I : (i : ι), finite_dimensional K (M i)] :
finite_dimensional K (Π (i : ι), M i)

A finite dimensional vector space over a finite field is finite

Equations
theorem finite_dimensional.of_fintype_basis {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module K V] {ι : Type w} [finite ι] (h : basis ι 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} [division_ring K] [add_comm_group V] [module K V] {ι : Type u_1} [finite_dimensional K V] (b : basis ι K V) :

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

Equations
@[protected, instance]

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} [division_ring K] [add_comm_group V] [module K V] {ι : Type w} {s : set ι} (h : basis s 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]

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

@[protected, instance]

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

In a finite-dimensional space, its dimension (seen as a cardinal) coincides with its finrank. This is a copy of finrank_eq_rank _ _ which creates easier typeclass searches.

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.

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

noncomputable def basis.unique {K : Type u} [division_ring K] {ι : Type u_1} (b : basis ι K K) :

Given a basis of a division ring over itself indexed by a type ι, then ι is unique.

Equations

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

Equations
noncomputable def finite_dimensional.fin_basis_of_finrank_eq (K : Type u) (V : Type v) [division_ring K] [add_comm_group V] [module K V] [finite_dimensional K V] {n : } (hn : finite_dimensional.finrank K V = 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} [division_ring K] [add_comm_group V] [module K V] (ι : Type u_1) [unique ι] (h : finite_dimensional.finrank K V = 1) :
basis ι 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} [division_ring K] [add_comm_group V] [module K V] {ι : Type u_1} [unique ι] {h : finite_dimensional.finrank K V = 1} {v : V} {i : ι} :
theorem linear_independent.finite {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module K V] [finite_dimensional K V] {b : set V} (h : linear_independent K (λ (x : b), x)) :

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

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

A nontrivial finite dimensional space has positive finrank.

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

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

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

@[protected, instance]

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

@[protected, instance]

The submodule generated by a finset is finite-dimensional.

@[protected, instance]

Pushforwards of finite-dimensional submodules are finite-dimensional.

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

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_rank_lt_card {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module K V] [finite_dimensional K V] {t : finset V} (h : finite_dimensional.finrank K V < 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_rank_succ_lt_card {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module K V] [finite_dimensional K V] {t : finset V} (h : finite_dimensional.finrank K V + 1 < 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_rank_succ_lt_card {L : Type u_1} [linear_ordered_field L] {W : Type v} [add_comm_group W] [module L W] [finite_dimensional L W] {t : finset W} (h : finite_dimensional.finrank L W + 1 < 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_rank_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_symm_apply {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module K V] (ι : Type u_1) [unique ι] (h : finite_dimensional.finrank K V = 1) (v : V) (hv : v 0) (f : ι →₀ K) :
noncomputable def finite_dimensional.basis_singleton {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module K V] (ι : Type u_1) [unique ι] (h : finite_dimensional.finrank K V = 1) (v : V) (hv : v 0) :
basis ι 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} [division_ring K] [add_comm_group V] [module K V] (ι : Type u_1) [unique ι] (h : finite_dimensional.finrank K V = 1) (v : V) (hv : v 0) (i : ι) :
@[simp]
theorem finite_dimensional.range_basis_singleton {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module K V] (ι : Type u_1) [unique ι] (h : finite_dimensional.finrank K V = 1) (v : V) (hv : v 0) :
@[protected, instance]
theorem bot_eq_top_of_rank_eq_zero {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module K V] (h : module.rank K V = 0) :
@[simp]
theorem rank_eq_zero {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module K V] {S : submodule K V} :
@[simp]

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} [division_ring K] [add_comm_group V] [module K V] {S₁ S₂ : submodule K V} [finite_dimensional K 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} [division_ring K] [add_comm_group V] [module K V] (S₁ S₂ : submodule K V) [finite_dimensional K 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} [division_ring K] [add_comm_group V] [module K V] (S₁ S₂ : submodule K V) [finite_dimensional K 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} [division_ring K] [add_comm_group V] [module K V] (S₁ S₂ : submodule K V) [h₁ : finite_dimensional K S₁] [h₂ : finite_dimensional K 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} [division_ring K] [add_comm_group V] [module K V] {ι : Type u_1} (s : finset ι) (S : ι submodule K V) [ (i : ι), finite_dimensional K (S i)] :

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} [division_ring K] [add_comm_group V] [module K V] {ι : Sort u_1} [finite ι] (S : ι submodule K V) [ (i : ι), finite_dimensional K (S i)] :
finite_dimensional K ( (i : ι), S i)

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

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

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

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

@[protected]
theorem linear_equiv.finite_dimensional {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module K V] {V₂ : Type v'} [add_comm_group V₂] [module K V₂] (f : V ≃ₗ[K] V₂) [finite_dimensional K V] :

Finite dimensionality is preserved under linear equivalence.

@[protected, instance]
def finite_dimensional_finsupp {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module K V] {ι : Type u_1} [finite ι] [h : finite_dimensional K V] :
theorem finite_dimensional.eq_of_le_of_finrank_le {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module K V] {S₁ S₂ : submodule K V} [finite_dimensional K S₂] (hle : S₁ S₂) (hd : finite_dimensional.finrank K S₂ finite_dimensional.finrank K S₁) :
S₁ = S₂
theorem finite_dimensional.eq_of_le_of_finrank_eq {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module K V] {S₁ S₂ : submodule K V} [finite_dimensional K S₂] (hle : S₁ S₂) (hd : finite_dimensional.finrank K S₁ = finite_dimensional.finrank K S₂) :
S₁ = S₂

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

noncomputable def finite_dimensional.linear_equiv.quot_equiv_of_equiv {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module K V] {V₂ : Type v'} [add_comm_group V₂] [module K V₂] [finite_dimensional K V] [finite_dimensional K V₂] {p : subspace K V} {q : subspace K 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} [division_ring K] [add_comm_group V] [module K V] [finite_dimensional K V] {p q : subspace K 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

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

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

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

@[protected, instance]

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

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

theorem linear_map.mul_eq_one_of_mul_eq_one {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module K V] [finite_dimensional K 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} [division_ring K] [add_comm_group V] [module K V] [finite_dimensional K 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.

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.

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} [division_ring K] [add_comm_group V] [module K V] [finite_dimensional K V] (f : V →ₗ[K] V) (h_inj : function.injective f) :

The linear equivalence corresponging to an injective endomorphism.

Equations
noncomputable def basis_of_finrank_zero {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module K V] [finite_dimensional K V] {ι : Type u_1} [is_empty ι] (hV : finite_dimensional.finrank K V = 0) :
basis ι K V

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

Equations
noncomputable def linear_map.linear_equiv_of_injective {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module K V] {V₂ : Type v'} [add_comm_group V₂] [module K V₂] [finite_dimensional K V] [finite_dimensional K V₂] (f : V →ₗ[K] V₂) (hf : function.injective f) (hdim : finite_dimensional.finrank K V = finite_dimensional.finrank K V₂) :
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
@[simp]
theorem linear_map.linear_equiv_of_injective_apply {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module K V] {V₂ : Type v'} [add_comm_group V₂] [module K V₂] [finite_dimensional K V] [finite_dimensional K V₂] {f : V →ₗ[K] V₂} (hf : function.injective f) (hdim : finite_dimensional.finrank K V = finite_dimensional.finrank K V₂) (x : V) :
noncomputable def division_ring_of_finite_dimensional (F : Type u_1) (K : Type u_2) [field F] [ring K] [is_domain K] [algebra F K] [finite_dimensional F 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] [algebra F K] [finite_dimensional F K] :

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

Equations
theorem finrank_span_singleton {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module K V] {v : V} (hv : v 0) :
theorem set.finrank_mono {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module K V] [finite_dimensional K V] {s t : set V} (h : s t) :
theorem span_eq_top_of_linear_independent_of_card_eq_finrank {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module K V] {ι : Type u_1} [hι : nonempty ι] [fintype ι] {b : ι V} (lin_ind : linear_independent K b) (card_eq : fintype.card ι = finite_dimensional.finrank K V) :
noncomputable def basis_of_linear_independent_of_card_eq_finrank {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module K V] {ι : Type u_1} [nonempty ι] [fintype ι] {b : ι V} (lin_ind : linear_independent K b) (card_eq : fintype.card ι = finite_dimensional.finrank K V) :
basis ι 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_symm_apply {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module K V] {ι : Type u_1} [nonempty ι] [fintype ι] {b : ι V} (lin_ind : linear_independent K b) (card_eq : fintype.card ι = finite_dimensional.finrank K V) (ᾰ : ι →₀ K) :
@[simp]
@[simp]
theorem finset_basis_of_linear_independent_of_card_eq_finrank_repr_symm_apply {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module K V] {s : finset V} (hs : s.nonempty) (lin_ind : linear_independent K coe) (card_eq : s.card = finite_dimensional.finrank K V) (ᾰ : {x // x s} →₀ K) :
noncomputable def finset_basis_of_linear_independent_of_card_eq_finrank {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module K V] {s : finset V} (hs : s.nonempty) (lin_ind : linear_independent K coe) (card_eq : s.card = finite_dimensional.finrank K V) :
basis s K V

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

Equations

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

Equations

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

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

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} [division_ring K] [add_comm_group V] [module K V] (v : V) (nz : v 0) :
finite_dimensional.finrank K V = 1 (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} [division_ring K] [add_comm_group V] [module K V] (ι : Type u_1) [unique ι] :

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} [division_ring K] [add_comm_group V] [module K V] :
finite_dimensional.finrank K V = 1 (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} [division_ring K] [add_comm_group V] [module K V] [finite_dimensional K V] :
finite_dimensional.finrank K V 1 (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 surjective_of_nonzero_of_finrank_eq_one {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module K V] {W : Type u_1} {A : Type u_2} [semiring A] [module A V] [add_comm_group W] [module K W] [module A W] [linear_map.compatible_smul V W K A] (h : finite_dimensional.finrank K W = 1) {f : V →ₗ[A] W} (w : f 0) :

Any K-algebra module that is 1-dimensional over K is simple.

A subalgebra is finite_dimensional iff it is finite_dimensional as a submodule.

@[protected, instance]
@[protected, instance]
theorem subalgebra.eq_bot_of_rank_le_one {F : Type u_1} {E : Type u_2} [field F] [ring E] [algebra F E] {S : subalgebra F E} (h : module.rank F S 1) :
S =
theorem subalgebra.eq_bot_of_finrank_one {F : Type u_1} {E : Type u_2} [field F] [ring E] [algebra F E] {S : subalgebra F E} (h : finite_dimensional.finrank F S = 1) :
S =
@[simp]
theorem subalgebra.rank_eq_one_iff {F : Type u_1} {E : Type u_2} [field F] [ring E] [algebra F E] [nontrivial E] {S : subalgebra F E} :
@[simp]
theorem subalgebra.finrank_eq_one_iff {F : Type u_1} {E : Type u_2} [field F] [ring E] [algebra F E] [nontrivial E] {S : subalgebra F E} :
theorem subalgebra.bot_eq_top_iff_rank_eq_one {F : Type u_1} {E : Type u_2} [field F] [ring E] [algebra F E] [nontrivial E] :
@[simp]
theorem subalgebra.bot_eq_top_of_rank_eq_one {F : Type u_1} {E : Type u_2} [field F] [ring E] [algebra F E] [nontrivial E] :

Alias of the reverse direction of subalgebra.bot_eq_top_iff_rank_eq_one.

@[simp]

Alias of the reverse direction of subalgebra.bot_eq_top_iff_finrank_eq_one.

theorem module.End.ker_pow_constant {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module K V] {f : module.End K V} {k : } (h : linear_map.ker (f ^ k) = linear_map.ker (f ^ k.succ)) (m : ) :