Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-09 11:14 aaab1139

View on Github →

refactor(linear_algebra/prod): split out prod and coprod defs and lemmas (#6059) Lemmas are moved without modification. I expect this will take a few builds of adding missing imports.

Estimated changes

deleted theorem linear_equiv.coe_prod
deleted theorem linear_equiv.prod_apply
deleted theorem linear_equiv.prod_symm
deleted theorem linear_map.comp_coprod
deleted def linear_map.coprod
deleted theorem linear_map.coprod_apply
deleted theorem linear_map.coprod_inl
deleted theorem linear_map.coprod_inl_inr
deleted theorem linear_map.coprod_inr
deleted def linear_map.fst
deleted theorem linear_map.fst_apply
deleted theorem linear_map.fst_eq_coprod
deleted theorem linear_map.fst_prod
deleted def linear_map.inl
deleted theorem linear_map.inl_apply
deleted theorem linear_map.inl_eq_prod
deleted theorem linear_map.inl_injective
deleted def linear_map.inr
deleted theorem linear_map.inr_apply
deleted theorem linear_map.inr_eq_prod
deleted theorem linear_map.inr_injective
deleted theorem linear_map.ker_prod
deleted theorem linear_map.pair_fst_snd
deleted def linear_map.prod
deleted def linear_map.prod_map
deleted theorem linear_map.prod_map_apply
deleted theorem linear_map.range_coprod
deleted theorem linear_map.range_prod_eq
deleted theorem linear_map.range_prod_le
deleted def linear_map.snd
deleted theorem linear_map.snd_apply
deleted theorem linear_map.snd_eq_coprod
deleted theorem linear_map.snd_prod
deleted theorem submodule.comap_fst
deleted theorem submodule.comap_snd
deleted theorem submodule.ker_inl
deleted theorem submodule.ker_inr
deleted theorem submodule.map_inl
deleted theorem submodule.map_inr
deleted theorem submodule.prod_comap_inl
deleted theorem submodule.prod_comap_inr
deleted theorem submodule.prod_map_fst
deleted theorem submodule.prod_map_snd
deleted theorem submodule.range_fst
deleted theorem submodule.range_snd
deleted theorem submodule.sup_eq_range
added theorem linear_equiv.coe_prod
added theorem linear_equiv.prod_symm
added theorem linear_map.comp_coprod
added theorem linear_map.coprod_inl
added theorem linear_map.coprod_inr
added def linear_map.fst
added theorem linear_map.fst_apply
added theorem linear_map.fst_prod
added def linear_map.inl
added theorem linear_map.inl_apply
added theorem linear_map.inl_eq_prod
added def linear_map.inr
added theorem linear_map.inr_apply
added theorem linear_map.inr_eq_prod
added theorem linear_map.ker_prod
added def linear_map.prod
added def linear_map.snd
added theorem linear_map.snd_apply
added theorem linear_map.snd_prod
added theorem submodule.comap_fst
added theorem submodule.comap_snd
added theorem submodule.ker_inl
added theorem submodule.ker_inr
added theorem submodule.map_inl
added theorem submodule.map_inr
added theorem submodule.prod_map_fst
added theorem submodule.prod_map_snd
added theorem submodule.range_fst
added theorem submodule.range_snd
added theorem submodule.sup_eq_range