Commit 2024-02-14 03:21 e50aeb4d

View on Github →

chore: Move LinearMap.ker to a new file (#10233) This shortens Mathlib.LinearAlgebra.Basic, which is both longer than we like and doesn't have a clear scope.

Estimated changes

added theorem LinearEquiv.ker_comp
added theorem LinearMap.disjoint_ker
added def LinearMap.ker
added theorem LinearMap.ker_comp
added theorem LinearMap.ker_eq_bot'
added theorem LinearMap.ker_eq_bot
added theorem LinearMap.ker_eq_top
added theorem LinearMap.ker_id
added theorem LinearMap.ker_le_comap
added theorem LinearMap.ker_restrict
added theorem LinearMap.ker_smul'
added theorem LinearMap.ker_smul
added theorem LinearMap.ker_zero
added theorem LinearMap.map_coe_ker
added theorem LinearMap.mem_ker
added theorem Submodule.comap_bot
added theorem Submodule.ker_subtype
deleted theorem LinearEquiv.ker_comp
deleted theorem LinearEquiv.map_eq_comap
deleted theorem LinearMap.disjoint_ker'
deleted theorem LinearMap.disjoint_ker
deleted def LinearMap.ker
deleted theorem LinearMap.ker_codRestrict
deleted theorem LinearMap.ker_comp
deleted theorem LinearMap.ker_eq_bot'
deleted theorem LinearMap.ker_eq_bot
deleted theorem LinearMap.ker_eq_top
deleted theorem LinearMap.ker_id
deleted theorem LinearMap.ker_le_comap
deleted theorem LinearMap.ker_le_ker_comp
deleted theorem LinearMap.ker_restrict
deleted theorem LinearMap.ker_smul'
deleted theorem LinearMap.ker_smul
deleted theorem LinearMap.ker_zero
deleted theorem LinearMap.le_ker_iff_map
deleted theorem LinearMap.map_codRestrict
deleted theorem LinearMap.map_coe_ker
deleted theorem LinearMap.mem_ker
deleted theorem LinearMap.sub_mem_ker_iff
deleted theorem LinearMapClass.ker_eq_bot
deleted theorem Submodule.comap_bot
deleted theorem Submodule.ker_inclusion
deleted theorem Submodule.ker_subtype