feat(linear_algebra/eigenspace): generalized eigenvectors span the entire space (#4111)

Author: abentkamp

docs/references.bib

@@ -4,6 +4,19 @@
 %                                                                     %
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
+@book{axler2015,
+ Author = {Sheldon Axler},
+ Title = {Linear algebra done right. 3rd ed.},
+ FJournal = {Undergraduate Texts in Mathematics},
+ Journal = {Undergraduate Texts Math.},
+ ISSN = {0172-6056; 2197-5604/e},
+ Edition = {3rd ed.},
+ ISBN = {978-3-319-11079-0/hbk; 978-3-319-11080-6/ebook},
+ Pages = {xvii + 340},
+ Year = {2015},
+ Publisher = {Springer},
+}
+
 @article {MR1167694,
     AUTHOR = {Blass, Andreas},
      TITLE = {A game semantics for linear logic},

src/linear_algebra/basic.lean

@@ -1221,6 +1221,10 @@ lemma range_cod_restrict (p : submodule R M) (f : M₂ →ₗ[R] M) (hf) :
   range (cod_restrict p f hf) = comap p.subtype f.range :=
 map_cod_restrict _ _ _ _
 
+lemma ker_restrict {p : submodule R M} {f : M →ₗ[R] M} (hf : ∀ x : M, x ∈ p → f x ∈ p) :
+  ker (f.restrict hf) = (f.dom_restrict p).ker :=
+by rw [restrict_eq_cod_restrict_dom_restrict, ker_cod_restrict]
+
 lemma map_comap_eq (f : M →ₗ[R] M₂) (q : submodule R M₂) :
   map f (comap f q) = range f ⊓ q :=
 le_antisymm (le_inf (map_mono le_top) (map_comap_le _ _)) $