Commit 2023-11-03 19:29 ccd15763

View on Github →

feat: miscellaneous linear algebra lemmas (#8157)

Estimated changes

Modified Mathlib/Algebra/Algebra/Basic.lean

added theorem Algebra.commute_algebraMap_left

added theorem Algebra.commute_algebraMap_right

Modified Mathlib/Algebra/Module/Submodule/Lattice.lean

modified theorem Submodule.eq_bot_of_subsingleton

added theorem Submodule.nontrivial_iff_ne_bot

added theorem Submodule.subsingleton_iff_eq_bot

Modified Mathlib/Analysis/InnerProductSpace/Spectrum.lean

Modified Mathlib/Data/Set/Function.lean

added theorem Set.MapsTo.restrict_surjective_iff

Modified Mathlib/LinearAlgebra/Basic.lean

added theorem LinearMap.injective_restrict_iff_disjoint

added theorem LinearMap.ker_le_comap

added theorem LinearMap.ker_sup_ker_le_ker_comp_of_commute

Modified Mathlib/LinearAlgebra/DFinsupp.lean

added theorem Submodule.mem_iSup_iff_exists_finsupp

Modified Mathlib/LinearAlgebra/FiniteDimensional.lean

added theorem LinearMap.comap_eq_sup_ker_of_disjoint

added theorem LinearMap.injOn_iff_surjOn

added theorem LinearMap.ker_comp_eq_of_commute_of_disjoint_ker

added theorem LinearMap.ker_noncommProd_eq_of_supIndep_ker

Modified Mathlib/LinearAlgebra/Matrix/Gershgorin.lean