Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-26 13:13 47b62ea4

View on Github →

feat(algebra/big_operators): add lemmas about sum and pi.single (#6390)

Estimated changes

Modified src/algebra/big_operators/basic.lean

added theorem finset.sum_pi_single'

added theorem finset.sum_pi_single

Modified src/algebra/big_operators/pi.lean

modified theorem ring_hom.functions_ext

Modified src/algebra/module/linear_map.lean

added theorem linear_map.ext_ring_iff

Modified src/algebra/module/pi.lean

modified theorem pi.single_smul'

modified theorem pi.single_smul

Modified src/linear_algebra/pi.lean

Modified src/topology/algebra/module.lean

added theorem continuous_linear_map.coe_pi'

modified theorem continuous_linear_map.coe_pi