Commit 2024-06-08 08:17 1808f157

View on Github →

chore: move LinearMap.eqLocus to its own file (#13566)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Module/Submodule/EqLocus.lean

added def LinearMap.eqLocus

added theorem LinearMap.eqLocus_eq_ker_sub

added theorem LinearMap.eqLocus_eq_top

added theorem LinearMap.eqLocus_same

added theorem LinearMap.eqLocus_toAddSubmonoid

added theorem LinearMap.eqOn_sup

added theorem LinearMap.ext_on_codisjoint

added theorem LinearMap.le_eqLocus

added theorem LinearMap.mem_eqLocus

Modified Mathlib/LinearAlgebra/Basic.lean

deleted def LinearMap.eqLocus

deleted theorem LinearMap.eqLocus_eq_ker_sub

deleted theorem LinearMap.eqLocus_eq_top

deleted theorem LinearMap.eqLocus_same

deleted theorem LinearMap.eqLocus_toAddSubmonoid

deleted theorem LinearMap.eqOn_sup

deleted theorem LinearMap.ext_on_codisjoint

deleted theorem LinearMap.le_eqLocus

deleted theorem LinearMap.mem_eqLocus

Modified Mathlib/LinearAlgebra/Span.lean