Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-18 21:20 34020e53

View on Github →

chore(linear_algebra/basic): generalize submodule.map, comap, etc to semilinear_map_class (#16105) This PR generalizes submodule.map, submodule.comap, linear_map.ker and linear_map.range such that they are defined for any morphism class satisfying semilinear_map_class (they are currently hardcoded for linear_maps). The namespaces have been left as is.

Estimated changes

modified def submodule.torsion_by
modified theorem linear_isometry.nnnorm_map
modified theorem linear_isometry.norm_map
modified theorem linear_map.comap_injective
modified theorem linear_map.disjoint_ker
modified def linear_map.ker
modified theorem linear_map.ker_eq_bot'
modified theorem linear_map.le_ker_iff_map
modified theorem linear_map.map_coe_ker
modified theorem linear_map.map_le_range
modified theorem linear_map.mem_ker
modified def linear_map.range
modified theorem linear_map.range_coe
modified theorem linear_map.range_eq_top
modified theorem submodule.apply_coe_mem_map
modified def submodule.comap
modified theorem submodule.comap_bot
modified theorem submodule.comap_coe
modified theorem submodule.comap_id
modified theorem submodule.comap_inf
modified theorem submodule.comap_infi
modified theorem submodule.comap_mono
modified theorem submodule.comap_top
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_mono
modified theorem submodule.map_sup
modified theorem submodule.map_supr
modified theorem submodule.map_top
modified theorem submodule.mem_comap
modified theorem submodule.mem_map
modified theorem submodule.mem_map_of_mem
modified theorem linear_map.infi_ker_proj
modified theorem submodule.binfi_comap_proj
modified theorem submodule.infi_comap_proj
modified theorem submodule.mapq_id
modified theorem linear_map.map_eq_top_iff
modified theorem linear_map.map_injective
modified theorem linear_map.map_le_map_iff'
modified theorem submodule.comap_map_eq
modified theorem submodule.comap_map_eq_self
modified theorem submodule.mem_annihilator'
modified theorem submodule.mem_colon'