Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-07 18:46 bdce1956

View on Github →

chore(linear_algebra/basic): review (#2616)

several new simp lemmas;
use linear_equiv.coe_coe instead of coe_apply;
rename sup_quotient_to_quotient_inf to quotient_inf_to_sup_quotient because it better reflects the definition; similarly for equiv.
make general_linear_group reducible.

Estimated changes

Modified src/algebra/module.lean

added theorem submodule.coe_eq_coe

added theorem submodule.coe_eq_zero

added theorem submodule.coe_mem

modified theorem submodule.mk_eq_zero

modified theorem submodule.neg_mem_iff

modified theorem submodule.smul_mem_iff'

Modified src/analysis/convex/cone.lean

Modified src/analysis/normed_space/finite_dimension.lean

Modified src/linear_algebra/basic.lean

deleted theorem linear_equiv.coe_apply

added theorem linear_equiv.coe_coe

added theorem linear_equiv.coe_to_add_equiv

added theorem linear_equiv.coe_to_equiv

added theorem linear_equiv.eq_symm_apply

added theorem linear_equiv.map_eq_comap

added theorem linear_equiv.refl_trans

added theorem linear_equiv.symm_apply_eq

added theorem linear_equiv.trans_refl

modified def linear_map.general_linear_group

added theorem linear_map.map_coe_ker

added theorem linear_map.mem_range_self

added def linear_map.quotient_inf_to_sup_quotient

added theorem linear_map.range_coprod

added def linear_map.range_restrict

deleted def linear_map.sup_quotient_to_quotient_inf

added theorem submodule.comap_subtype_eq_top

added theorem submodule.comap_subtype_self

modified theorem submodule.disjoint_iff_comap_eq_bot

modified theorem submodule.map_coe

added theorem submodule.mem_sup'

added theorem submodule.quot_hom_ext

added theorem submodule.range_range_restrict

added theorem submodule.sup_eq_range