Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-02-07 15:56 eeed3218

View on Github →

chore(linear_algebra/basic): relate map/comap/ker/range/comp with 0 and smul; use map/comap Galois connection

Estimated changes

added theorem linear_map.comp_assoc
modified theorem linear_map.comp_id
added theorem linear_map.comp_smul
added theorem linear_map.comp_zero
modified theorem linear_map.id_comp
added theorem linear_map.ker_smul'
added theorem linear_map.ker_smul
added theorem linear_map.range_smul'
added theorem linear_map.range_smul
added theorem linear_map.range_zero
added theorem linear_map.smul_comp
added theorem linear_map.zero_comp
added theorem submodule.comap_inf
added theorem submodule.comap_infi
added theorem submodule.comap_smul'
added theorem submodule.comap_smul
added theorem submodule.comap_zero
added theorem submodule.gc_map_comap
added theorem submodule.map_smul'
added theorem submodule.map_smul
added theorem submodule.map_sup
added theorem submodule.map_supr
added theorem submodule.map_zero