feat: Add Function.prod and Function.diag

[linesthatinterlace]

This PR adds Prod.diag, Prod.prodMk and Sum.get, canonical spellings of operations that are used in many places but only anonymously.

---

• depends on: feat: add Function.{prod,diag,fstComp,sndComp,prodMap} #37631

[github-actions]

PR summary 7d837a8020

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
There are 7213 files with changed transitive imports taking up over 319022 characters: this is too many to display!
You can run ci-tools/scripts/pr_summary/import_trans_difference.sh all locally to see the whole output.

---

Declarations diff

+ Continuous.fst_of_prod
+ Continuous.prod
+ Continuous.prod_left
+ Continuous.prod_right
+ Continuous.snd_of_prod
+ ContinuousAt.prod
+ Filter.Tendsto.prod_nhds
+ HasFunction.prod
+ Tendsto.prod
+ const_le_pair_iff
+ const_prod
+ continuous_prod
+ diag_apply
+ diag_eq_iff
+ exists_diag_apply_iff
+ fst_dcomp_pair
+ fst_diag
+ graphOn_prod
+ image2_flip
+ image_prodMap
+ injective_diag
+ leftInverse_uncurry_prod_prod_fst_comp_snd_comp
+ map_comp_diag
+ map_comp_prod
+ map_diag
+ map_prod
+ pair_le_const_iff
+ pair_le_pair_iff
+ piProdEquivProdPi
+ piProdEquivSumPi
+ preimage_prod
+ preimage_val_val_diagonal
+ prodMap
+ prodMap_eq_prod_map
+ prod_comp
+ prod_diag_diag
+ rightInverse_uncurry_prod_prod_fst_comp_snd_comp
+ snd_dcomp_pair
+ snd_diag
+ uncurry_apply
++ exists_fst_comp
++ exists_prod_apply_eq
++ exists_snd_comp
++ fst_comp_prod
++ fst_prod
++ prod_apply
++ prod_const_const
++ prod_eq_iff
++ prod_ext_iff
++ prod_fst_snd_comp
++ snd_comp_prod
++ snd_prod
+-+ diag
+-+ prod
+-+-+-+-+-+-+- coe_prod
- Continuous.prodMk_left
- Continuous.prodMk_right
- ContinuousAt.prodMk
- Filter.Tendsto.prodMk_nhds
- HasProd.prodMk
- Tendsto.prodMk
- continuous_prodMk
- sumArrowEquivProdArrow_apply_fst
- sumArrowEquivProdArrow_apply_snd
-++ prod_fst_snd
-++ prod_snd_fst

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[github-actions]

✅ PR Title Formatted Correctly

The title of this PR has been updated to match our commit style conventions.
Thank you!

[linesthatinterlace]

Note: I think Prod.pair is a better name than Prod.prodMk but I think that will be better as a follow-up PR as it will necessitate a lot of changes.

[linesthatinterlace]

Hmm - Pi.prod already exists but is frankly not consistently used and is not a great name for upstreaming.

[linesthatinterlace]

Decided to change to Function.prod and Function.diag to match usage elsewhere.

[linesthatinterlace]

It is clear that actually adapting this new notation/spelling into Mathlib is going to be somewhat time-consuming. That's fine but I think it will be easier to review if I split out the initial contribution. As such I have created #37631 and I am going to park this for now.

[grunweg]

(Recording the dependency in the PR description. Please correct me if I misread you!)

[mathlib-dependent-issues]

This PR/issue depends on:

• feat: add Function.{prod,diag,fstComp,sndComp,prodMap} #37631
  By Dependent Issues (🤖). Happy coding!

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[linesthatinterlace]

Closing this, better I think to finish this as a new PR.