feat(Analysis): add Commute.exp_smul_right and symmetric variants

[VictorBoscaro]

Summary

Adds Commute.exp_smul_right, Commute.exp_smul_left, and Commute.exp_smul
to Mathlib/Analysis/Normed/Algebra/Exponential.lean, immediately after
Commute.exp. One-line compositions of Commute.smul_* with Commute.exp_*.
Same typeclass scope as Commute.exp_right; no new hypotheses.

Context

Commute.exp_right / Commute.exp_left / Commute.exp handle the
Commute x (exp y) shape; Commute.smul_right / Commute.smul_left handle
Commute x (r • y). The natural composition Commute x (exp (r • y)) —
the canonical shape in one-parameter semigroups t ↦ exp (t • Q) — is absent
and currently requires inline chaining.

Notes

• One-line proofs; same typeclass scope as Commute.exp_right.
• No @[simp] / no @[to_additive] — matches the existing Commute.exp_* choices.
• API minimal — exp_smul_self, exp_nsmul_* can follow separately if needed.

Where this can be used

Existing Mathlib — concrete simplifications.
Mathlib/Analysis/SpecialFunctions/Exponential.lean:292, 313 write the chain
explicitly: (((Commute.refl x).smul_left t').smul_right t).exp_right would
compress to ((Commute.refl x).smul_left t').exp_smul_right t.

Mathlib/Analysis/CStarAlgebra/Fuglede.lean:76 uses
grind [exp_add_of_commute, Commute.smul_right, Commute.neg_right] to discharge
a commutation goal in the Fuglede–Putnam–Rosenblum proof; these lemmas would be
natural additions to that hint set.

Areas where this composition recurs.
The composition [P, Q] = 0 ⟹ [P, exp(t · Q)] = 0 appears in:

Area	Where the composition appears
Strongly continuous semigroups (Hille–Yosida)	P commutes with the infinitesimal generator Q ⟹ P commutes with e^{tQ}.
Stone's theorem	One-parameter unitary groups U(t) = exp(itA); commuting observables commute with the full evolution.
Markov semigroups	M_t = exp(tQ) for Q a Q-matrix; symmetries of Q lift to symmetries of M_t.
Lie group exponential	X, Y commuting in the Lie algebra ⟹ exp(tX), exp(sY) commute.
Functional calculus	f(A)g(A) = g(A)f(A) for commuting operators, with the exp specialisation at each step.
PDE flows	Heat / Schrödinger evolution: conservation laws are commutation with exp(t·Δ) / exp(-itH).
Tomita–Takesaki	The modular automorphism group σ^φ_t = Ad(Δ^{it}) on a von Neumann algebra.

[github-actions]

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

[github-actions]

PR summary 0bcf97ceb9

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ _root_.Commute.exp_smul
+ _root_.Commute.exp_smul_left
+ _root_.Commute.exp_smul_right

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to strong technical debt.

No changes to weak technical debt.

[mathlib-triage]

We appreciate your desire to contribute to mathlib. Unfortunately, this PR does not meet community standards.

Our reviewer time is very limited so we must prioritize both individuals who can learn and contribute back to the community and sufficiently high quality content as to make the process smooth and valuable.