Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-22 14:12 78eb83a3

View on Github →

feat(linear_algebra/pi): add pi.lsum (#6335)

Estimated changes

Modified src/linear_algebra/basic.lean

modified theorem linear_map.coe_fn_sum

Modified src/linear_algebra/pi.lean

added theorem linear_map.apply_single

added theorem linear_map.coe_single

added def linear_map.lsum

added theorem linear_map.pi_ext'

added theorem linear_map.pi_ext'_iff

added theorem linear_map.pi_ext

added theorem linear_map.pi_ext_iff

Modified src/linear_algebra/prod.lean

added theorem linear_map.coprod_comp_prod

Modified src/linear_algebra/std_basis.lean

deleted theorem linear_map.pi_ext'

deleted theorem linear_map.pi_ext'_iff

deleted theorem linear_map.pi_ext

deleted theorem linear_map.pi_ext_iff