Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-09 17:14 9648ce29

View on Github →

chore(data/pi): add pi.prod and use elsewhere (#11877) pi.prod is the function that underlies add_monoid_hom.prod, linear_map.prod, etc. Zulip thread

Estimated changes

Modified archive/sensitivity.lean

Modified src/algebra/big_operators/basic.lean

added theorem monoid_hom.coe_finset_prod

deleted theorem monoid_hom.coe_prod

Modified src/algebra/direct_sum/ring.lean

Modified src/algebra/group/prod.lean

added theorem monoid_hom.coe_prod

Modified src/algebra/triv_sq_zero_ext.lean

Modified src/data/dfinsupp/basic.lean

Modified src/data/finsupp/basic.lean

Modified src/data/pi.lean

added theorem pi.prod_fst_snd

added theorem pi.prod_snd_fst

Modified src/linear_algebra/dimension.lean

Modified src/linear_algebra/prod.lean

added theorem linear_map.coe_prod

Modified src/topology/algebra/group.lean