Commit 2021-02-08 16:17 1a0f84c7

View on Github →

feat(linear_algebra/basic): bundle prod and coprod into linear_equivs (#5992) In order to do this, this has to reorder some definitions to make the semimodule structure on linear maps available earlier.

Estimated changes

Modified src/linear_algebra/basic.lean

added theorem linear_map.comp_coprod

modified theorem linear_map.coprod_apply

added def linear_map.coprod_equiv

modified theorem linear_map.fst_eq_coprod

deleted theorem linear_map.is_linear_map_prod_iso

modified def linear_map.prod

deleted theorem linear_map.prod_apply

added def linear_map.prod_equiv

modified theorem linear_map.snd_eq_coprod