feat(RingTheory): base change of graded algebra

[kckennylau]

In this file we show that if 𝒜 is a graded R-algebra, and S is any R-algebra, then S ⊗[R] 𝒜 (which is actually fun i ↦ (𝒜 i).baseChange S) is a graded S-algebra with the same grading.

---

Split from #26061.

[github-actions]

PR summary c32a3cfc16

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.LinearAlgebra.TensorProduct.Decomposition (new file)	1029
Mathlib.RingTheory.GradedAlgebra.TensorProduct (new file)	1100

---

Declarations diff

+ Decomposition.baseChange
+ _root_.LinearEquiv.baseChange_symm_tmul
+ _root_.LinearEquiv.baseChange_tmul
+ algebraMap_apply
+ coeLinearMap_lof
+ coe_algebraMap_apply
+ decomposeLinearEquiv_apply_coe
+ decomposeLinearEquiv_symm_lof
+ id_apply
+ id_symm_apply
+ instance : Algebra ((𝒜 0).baseChange S) (S ⊗[R] A)
+ instance : Algebra S ((𝒜 0).baseChange S)
+ instance : CommRing ((𝒜 0).baseChange S)
+ instance : CommSemiring ((𝒜 0).baseChange S)
+ instance : Ring ((𝒜 0).baseChange S)
+ instance : Semiring ((𝒜 0).baseChange S)
+ lequivCongrLeft_lof
+ lequivCongrLeft_symm_lof
+ lid_apply
+ lid_symm_apply
+ toBaseChange
+ toBaseChange_apply_tmul_coe
+ toBaseChange_surjective
+ toBaseChange_surjective'
++ baseChange
++ toBaseChange_bijective
++ toBaseChange_injective

You can run this locally as follows

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

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

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

---

No changes to technical debt.

You can run this locally as

./scripts/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).