Documentation

Mathlib.LinearAlgebra.FiniteDimensional.Defs

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

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

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 FiniteDimensional. For basic results that do not need the FiniteDimensional class, import Mathlib.LinearAlgebra.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 LinearMap.injective_iff_surjective, and the equivalence between left-inverse and right-inverse in LinearMap.mul_eq_one_comm and LinearMap.comp_eq_id_comm.

Implementation notes #

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

You should not assume that there has been any effort to state lemmas as generally as possible.

Plenty of the results hold for general fg modules or notherian modules, and they can be found in Mathlib.LinearAlgebra.FreeModule.Finite.Rank and Mathlib.RingTheory.Noetherian.

@[reducible, inline]
abbrev FiniteDimensional (K : Type u_1) (V : Type u_2) [DivisionRing K] [AddCommGroup V] [Module K V] :

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

Equations
Instances For
    theorem FiniteDimensional.of_injective {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂] [Module K V₂] (f : V →ₗ[K] V₂) (w : Function.Injective f) [FiniteDimensional K V₂] :

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

    theorem FiniteDimensional.of_surjective {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂] [Module K V₂] (f : V →ₗ[K] V₂) (w : Function.Surjective f) [FiniteDimensional K V] :

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

    instance FiniteDimensional.finiteDimensional_pi (K : Type u) [DivisionRing K] {ι : Type u_1} [Finite ι] :
    FiniteDimensional K (ιK)
    Equations
    • =
    instance FiniteDimensional.finiteDimensional_pi' (K : Type u) [DivisionRing K] {ι : Type u_1} [Finite ι] (M : ιType u_2) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module K (M i)] [∀ (i : ι), FiniteDimensional K (M i)] :
    FiniteDimensional K ((i : ι) → M i)
    Equations
    • =
    noncomputable def FiniteDimensional.fintypeOfFintype (K : Type u) (V : Type v) [DivisionRing K] [AddCommGroup V] [Module K V] [Fintype K] [FiniteDimensional K V] :

    A finite dimensional vector space over a finite field is finite

    Equations
    Instances For
      theorem FiniteDimensional.of_fintype_basis {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup 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 FiniteDimensional.fintypeBasisIndex {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type u_1} [FiniteDimensional K V] (b : Basis ι K V) :

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

      Equations
      Instances For

        If a vector space is FiniteDimensional, Basis.ofVectorSpace is indexed by a finite type.

        Equations
        • FiniteDimensional.instFintypeElemOfVectorSpaceIndex = inferInstance
        theorem FiniteDimensional.of_finite_basis {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup 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.

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

        Equations
        • =

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

        Equations
        • =

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

        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.

        theorem Module.finrank_eq_card_basis' {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {ι : Type w} (h : Basis ι K V) :

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

        theorem Submodule.eq_top_of_finrank_eq {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {S : Submodule K V} (h : Module.finrank K S = Module.finrank K V) :
        S =

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

        theorem FiniteDimensional.span_of_finite (K : Type u) {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {A : Set V} (hA : A.Finite) :

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

        instance FiniteDimensional.span_singleton (K : Type u) {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (x : V) :

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

        Equations
        • =
        instance FiniteDimensional.span_finset (K : Type u) {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (s : Finset V) :

        The submodule generated by a finset is finite-dimensional.

        Equations
        • =
        instance FiniteDimensional.instSubtypeMemSubmoduleMapLinearMapId (K : Type u) {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂] [Module K V₂] (f : V →ₗ[K] V₂) (p : Submodule K V) [FiniteDimensional K p] :

        Pushforwards of finite-dimensional submodules are finite-dimensional.

        Equations
        • =
        theorem FiniteDimensional.exists_relation_sum_zero_pos_coefficient_of_finrank_succ_lt_card {L : Type u_1} [LinearOrderedField L] {W : Type v} [AddCommGroup W] [Module L W] [FiniteDimensional L W] {t : Finset W} (h : Module.finrank L W + 1 < t.card) :
        ∃ (f : WL), et, f e e = 0 et, f e = 0 xt, 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 FiniteDimensional.basisSingleton_repr_apply {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (ι : Type u_1) [Unique ι] (h : Module.finrank K V = 1) (v : V) (hv : v 0) (w : V) :
        (FiniteDimensional.basisSingleton ι h v hv).repr w = Finsupp.single default (((Module.basisUnique ι h).repr w) default / ((Module.basisUnique ι h).repr v) default)
        noncomputable def FiniteDimensional.basisSingleton {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (ι : Type u_1) [Unique ι] (h : Module.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
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem FiniteDimensional.basisSingleton_apply {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (ι : Type u_1) [Unique ι] (h : Module.finrank K V = 1) (v : V) (hv : v 0) (i : ι) :
          @[simp]
          theorem FiniteDimensional.range_basisSingleton {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (ι : Type u_1) [Unique ι] (h : Module.finrank K V = 1) (v : V) (hv : v 0) :
          theorem FiniteDimensional.trans (F : Type u_1) (K : Type u_2) (A : Type u_3) [DivisionRing F] [DivisionRing K] [AddCommGroup A] [Module F K] [Module K A] [Module F A] [IsScalarTower F K A] [FiniteDimensional F K] [FiniteDimensional K A] :
          theorem FiniteDimensional.of_rank_eq_nat {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {n : } (h : Module.rank K V = n) :
          @[deprecated FiniteDimensional.of_rank_eq_nat]
          theorem finiteDimensional_of_rank_eq_nat {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {n : } (h : Module.rank K V = n) :

          Alias of FiniteDimensional.of_rank_eq_nat.

          @[deprecated FiniteDimensional.of_rank_eq_zero]

          Alias of FiniteDimensional.of_rank_eq_zero.

          @[deprecated FiniteDimensional.of_rank_eq_one]

          Alias of FiniteDimensional.of_rank_eq_one.

          Equations
          • =
          theorem Submodule.fg_iff_finiteDimensional {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (s : Submodule K V) :

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

          theorem Submodule.finiteDimensional_of_le {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {S₁ : Submodule K V} {S₂ : Submodule K V} [FiniteDimensional K S₂] (h : S₁ S₂) :

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

          instance Submodule.finiteDimensional_inf_left {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (S₁ : Submodule K V) (S₂ : Submodule K V) [FiniteDimensional K S₁] :
          FiniteDimensional K (S₁ S₂)

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

          Equations
          • =
          instance Submodule.finiteDimensional_inf_right {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (S₁ : Submodule K V) (S₂ : Submodule K V) [FiniteDimensional K S₂] :
          FiniteDimensional K (S₁ S₂)

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

          Equations
          • =
          instance Submodule.finiteDimensional_sup {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (S₁ : Submodule K V) (S₂ : Submodule K V) [h₁ : FiniteDimensional K S₁] [h₂ : FiniteDimensional K S₂] :
          FiniteDimensional K (S₁ S₂)

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

          Equations
          • =
          instance Submodule.finiteDimensional_finset_sup {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type u_1} (s : Finset ι) (S : ιSubmodule K V) [∀ (i : ι), FiniteDimensional K (S i)] :
          FiniteDimensional K (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, FiniteDimensional K (S i), but that doesn't work well with typeclass search.

          Equations
          • =
          instance Submodule.finiteDimensional_iSup {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Sort u_1} [Finite ι] (S : ιSubmodule K V) [∀ (i : ι), FiniteDimensional K (S i)] :
          FiniteDimensional K (⨆ (i : ι), S i)

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

          Equations
          • =
          theorem LinearEquiv.finiteDimensional {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂] [Module K V₂] (f : V ≃ₗ[K] V₂) [FiniteDimensional K V] :

          Finite dimensionality is preserved under linear equivalence.

          instance finiteDimensional_finsupp {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type u_1} [Finite ι] [FiniteDimensional K V] :
          Equations
          • =
          theorem Submodule.eq_of_le_of_finrank_le {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {S₁ : Submodule K V} {S₂ : Submodule K V} [FiniteDimensional K S₂] (hle : S₁ S₂) (hd : Module.finrank K S₂ Module.finrank K S₁) :
          S₁ = S₂

          If a submodule is contained in a finite-dimensional submodule with the same or smaller dimension, they are equal.

          theorem Submodule.eq_of_le_of_finrank_eq {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {S₁ : Submodule K V} {S₂ : Submodule K V} [FiniteDimensional K S₂] (hle : S₁ S₂) (hd : Module.finrank K S₁ = Module.finrank K S₂) :
          S₁ = S₂

          If a submodule is contained in a finite-dimensional submodule with the same dimension, they are equal.

          theorem Subalgebra.eq_of_le_of_finrank_le {K : Type u_1} {L : Type u_2} [Field K] [Ring L] [Algebra K L] {F : Subalgebra K L} {E : Subalgebra K L} [hfin : FiniteDimensional K E] (h_le : F E) (h_finrank : Module.finrank K E Module.finrank K F) :
          F = E

          If a subalgebra is contained in a finite-dimensional subalgebra with the same or smaller dimension, they are equal.

          theorem Subalgebra.eq_of_le_of_finrank_eq {K : Type u_1} {L : Type u_2} [Field K] [Ring L] [Algebra K L] {F : Subalgebra K L} {E : Subalgebra K L} [hfin : FiniteDimensional K E] (h_le : F E) (h_finrank : Module.finrank K F = Module.finrank K E) :
          F = E

          If a subalgebra is contained in a finite-dimensional subalgebra with the same dimension, they are equal.

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

          theorem LinearMap.finiteDimensional_of_surjective {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂] [Module K V₂] [FiniteDimensional K V] (f : V →ₗ[K] V₂) (hf : LinearMap.range f = ) :

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

          instance LinearMap.finiteDimensional_range {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂] [Module K V₂] [FiniteDimensional K V] (f : V →ₗ[K] V₂) :

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

          Equations
          • =

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

          theorem LinearMap.injOn_iff_surjOn {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {p : Submodule K V} [FiniteDimensional K p] {f : V →ₗ[K] V} (h : xp, f x p) :
          Set.InjOn f p Set.SurjOn f p p
          theorem LinearMap.mul_eq_one_of_mul_eq_one {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f : V →ₗ[K] V} {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 LinearMap.mul_eq_one_comm {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f : V →ₗ[K] V} {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 LinearMap.comp_eq_id_comm {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f : V →ₗ[K] V} {g : V →ₗ[K] V} :
          f ∘ₗ g = LinearMap.id g ∘ₗ f = LinearMap.id

          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 LinearMap.comap_eq_sup_ker_of_disjoint {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {p : Submodule K V} [FiniteDimensional K p] {f : V →ₗ[K] V} (h : xp, f x p) (h' : Disjoint p (LinearMap.ker f)) :
          theorem LinearMap.ker_noncommProd_eq_of_supIndep_ker {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {ι : Type u_1} {f : ιV →ₗ[K] V} (s : Finset ι) (comm : (↑s).Pairwise fun (a b : ι) => Commute (f a) (f b)) (h : s.SupIndep fun (i : ι) => LinearMap.ker (f i)) :
          LinearMap.ker (s.noncommProd f comm) = is, LinearMap.ker (f i)
          noncomputable def LinearEquiv.ofInjectiveEndo {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : V →ₗ[K] V) (h_inj : Function.Injective f) :

          The linear equivalence corresponding to an injective endomorphism.

          Equations
          Instances For
            @[simp]
            theorem LinearEquiv.coe_ofInjectiveEndo {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : V →ₗ[K] V) (h_inj : Function.Injective f) :
            (LinearEquiv.ofInjectiveEndo f h_inj) = f
            @[simp]
            theorem LinearEquiv.ofInjectiveEndo_right_inv {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : V →ₗ[K] V) (h_inj : Function.Injective f) :
            f * (LinearEquiv.ofInjectiveEndo f h_inj).symm = 1
            @[simp]
            theorem LinearEquiv.ofInjectiveEndo_left_inv {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : V →ₗ[K] V) (h_inj : Function.Injective f) :
            (LinearEquiv.ofInjectiveEndo f h_inj).symm * f = 1
            theorem finrank_zero_iff_forall_zero {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] :
            Module.finrank K V = 0 ∀ (x : V), x = 0
            noncomputable def basisOfFinrankZero {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {ι : Type u_1} [IsEmpty ι] (hV : Module.finrank K V = 0) :
            Basis ι K V

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

            Equations
            Instances For
              theorem FiniteDimensional.exists_mul_eq_one (F : Type u_1) {K : Type u_2} [Field F] [Ring K] [IsDomain K] [Algebra F K] [FiniteDimensional F K] {x : K} (H : x 0) :
              ∃ (y : K), x * y = 1
              noncomputable def divisionRingOfFiniteDimensional (F : Type u_1) (K : Type u_2) [Field F] [Ring K] [IsDomain K] [Algebra F K] [FiniteDimensional F K] :

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

              Equations
              Instances For
                theorem FiniteDimensional.isUnit (F : Type u_1) {K : Type u_2} [Field F] [Ring K] [IsDomain K] [Algebra F K] [FiniteDimensional F K] {x : K} (H : x 0) :
                noncomputable def fieldOfFiniteDimensional (F : Type u_1) (K : Type u_2) [Field F] [h : CommRing K] [IsDomain K] [Algebra F K] [FiniteDimensional F K] :

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

                Equations
                Instances For
                  theorem finrank_span_singleton {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {v : V} (hv : v 0) :
                  theorem exists_smul_eq_of_finrank_eq_one {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (h : Module.finrank K V = 1) {x : V} (hx : x 0) (y : V) :
                  ∃ (c : K), c x = y

                  In a one-dimensional space, any vector is a multiple of any nonzero vector

                  theorem Set.finrank_mono {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {s : Set V} {t : Set V} (h : s t) :

                  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} [DivisionRing K] [AddCommGroup 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} [DivisionRing K] [AddCommGroup V] [Module K V] (v : V) (nz : v 0) :
                  Module.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 surjective_of_nonzero_of_finrank_eq_one {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {W : Type u_1} {A : Type u_2} [Semiring A] [Module A V] [AddCommGroup W] [Module K W] [Module A W] [LinearMap.CompatibleSMul V W K A] (h : Module.finrank K W = 1) {f : V →ₗ[A] W} (w : f 0) :
                  theorem Subalgebra.finiteDimensional_toSubmodule {F : Type u_1} {E : Type u_2} [Field F] [Ring E] [Algebra F E] {S : Subalgebra F E} :
                  FiniteDimensional F (Subalgebra.toSubmodule S) FiniteDimensional F S

                  A Subalgebra is FiniteDimensional iff it is FiniteDimensional as a submodule.

                  theorem FiniteDimensional.subalgebra_toSubmodule {F : Type u_1} {E : Type u_2} [Field F] [Ring E] [Algebra F E] {S : Subalgebra F E} :
                  FiniteDimensional F SFiniteDimensional F (Subalgebra.toSubmodule S)

                  Alias of the reverse direction of Subalgebra.finiteDimensional_toSubmodule.


                  A Subalgebra is FiniteDimensional iff it is FiniteDimensional as a submodule.

                  theorem FiniteDimensional.of_subalgebra_toSubmodule {F : Type u_1} {E : Type u_2} [Field F] [Ring E] [Algebra F E] {S : Subalgebra F E} :
                  FiniteDimensional F (Subalgebra.toSubmodule S)FiniteDimensional F S

                  Alias of the forward direction of Subalgebra.finiteDimensional_toSubmodule.


                  A Subalgebra is FiniteDimensional iff it is FiniteDimensional as a submodule.

                  Equations
                  • =
                  @[deprecated Subalgebra.finite_bot]
                  theorem Subalgebra.finiteDimensional_bot {F : Type u_1} {E : Type u_2} [Field F] [Ring E] [Algebra F E] :
                  theorem Module.End.ker_pow_constant {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {f : Module.End K V} {k : } (h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)) (m : ) :
                  LinearMap.ker (f ^ k) = LinearMap.ker (f ^ (k + m))