Commit 2025-12-27 09:40 c85f12d2

View on Github →

chore(*): restrict operations to LinearMaps (#33241) Make LinearMap.ker, LinearMap.range, Submodule.map, and Submodule.comap work for LinearMaps only.

Estimated changes

modified theorem LinearMap.disjoint_ker
modified def LinearMap.ker
modified theorem LinearMap.ker_eq_bot'
modified theorem LinearMap.ker_eq_bot
modified theorem LinearMap.le_ker_iff_map
modified theorem LinearMap.map_coe_ker
modified theorem LinearMap.mem_ker
deleted theorem LinearMapClass.ker_eq_bot
modified theorem Submodule.comap_bot
modified theorem Submodule.apply_coe_mem_map
modified def Submodule.comap
modified theorem Submodule.comap_coe
modified theorem Submodule.comap_iInf
modified theorem Submodule.comap_inf
modified theorem Submodule.comap_mono
modified theorem Submodule.comap_top
modified theorem Submodule.disjoint_map
modified theorem Submodule.gc_map_comap
modified theorem Submodule.le_comap_map
modified def Submodule.map
modified theorem Submodule.map_bot
modified theorem Submodule.map_coe
modified theorem Submodule.map_comap_le
modified theorem Submodule.map_iInf
modified theorem Submodule.map_iSup
modified theorem Submodule.map_inf
modified theorem Submodule.map_inf_le
modified theorem Submodule.map_mono
modified theorem Submodule.map_sup
modified theorem Submodule.mem_comap
modified theorem Submodule.mem_map
modified theorem Submodule.mem_map_of_mem
modified theorem LinearMap.coe_range
modified theorem LinearMap.comap_injective
modified theorem LinearMap.map_le_range
modified theorem LinearMap.mem_range
modified theorem LinearMap.mem_range_self
modified def LinearMap.range
modified theorem LinearMap.range_eq_map
modified theorem LinearMap.range_eq_top
modified theorem Submodule.codisjoint_map
modified theorem Submodule.map_comap_eq
modified theorem Submodule.map_comap_eq_self
modified theorem Submodule.map_top
modified theorem IsCoercive.isClosed_range
modified theorem IsCoercive.ker_eq_bot
modified theorem IsCoercive.range_eq_top
modified theorem Submodule.IsOrtho.comap_iff
modified theorem Submodule.IsOrtho.map
modified theorem Submodule.IsOrtho.map_iff
modified theorem Submodule.map_orthogonal
modified theorem LinearPMap.inverse_graph
modified theorem LinearMap.eqOn_span'
modified theorem LinearMap.eqOn_span
modified theorem LinearMap.eqOn_span_iff
modified theorem LinearMap.ext_on
modified theorem LinearMap.ext_on_range
modified theorem LinearMap.map_eq_top_iff
modified theorem LinearMap.map_injective
modified theorem LinearMap.map_le_map_iff'
modified theorem Submodule.comap_map_eq
modified theorem Submodule.comap_map_eq_self
modified theorem Submodule.image_span_subset
modified theorem Submodule.map_span
modified theorem Submodule.map_span_le
modified theorem Submodule.mapsTo_span
deleted theorem Submodule.span_image'
modified theorem Submodule.span_image
modified theorem Submodule.span_preimage_le
modified theorem Submodule.ker_subtypeL
modified theorem Submodule.range_subtypeL