feat(RingTheory/LaurentSeries): leibniz product rule for derivative

[localparty]

This PR adds the Leibniz product rule ((f * g)' = f' * g + f * g') for the
first formal derivative on LaurentSeries R (R a commutative ring).

The first derivative is already packaged in
Mathlib/RingTheory/LaurentSeries.lean as

def derivative (R : Type*) {V : Type*} [AddCommGroup V] [Semiring R] [Module R V] :
    LaurentSeries V →ₗ[R] LaurentSeries V :=
  hasseDeriv R 1

with a derivative_* family of theorems (derivative_apply,
derivative_iterate, derivative_iterate_coeff). The Leibniz product rule
was missing. This PR fills that gap, adding derivative_mul alongside the
existing derivative_* family.

The proof is direct on coefficients via HahnSeries.coeff_mul and an
addAntidiagonal shift-bijection (matching the style of the existing
hasseDeriv_* lemmas). Five private helper lemmas factor the
coefficient-side calculation:

• derivative_coeff — clean coefficient formula at k = 1
• support_derivative_subset — (derivative R f).support ⊆ (· - 1) '' f.support
• isPWO_shifted_support — PWO preserved by the shift-by-(-1)
• sum_bij_left / sum_bij_right — Finset.sum_nbij' shift-reindexings

Total addition: ~85 LOC (5 private helpers + the public derivative_mul).

Related future work

Full Derivation packaging for LaurentSeries.hasseDeriv (matching
PowerSeries.derivative-as-Derivation at
Mathlib/RingTheory/PowerSeries/Derivative.lean:102) is a natural follow-up,
since this Leibniz rule would discharge the leibniz' field. Out of scope
for this PR; can be a separate follow-up "LaurentSeries algebra-of-derivations
API" PR.

Provenance

This lemma surfaced during work on a Lean 4 formalization of equisingular
flat connections (Connes–Marcolli 2008, Ch IV §6.4), where LaurentSeries ℂ
serves as the base ring for the ℂ((t))-module connection-matrix substrate.
The Leibniz rule is needed for the category-of-connection-preserving-maps
intertwining condition.

[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 501b2af9ed

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ derivative_coeff
+ derivative_mul
+ hasseDeriv_one_mul
+ isPWO_shifted_support
+ sum_bij_left
+ sum_bij_right
+ support_derivative_subset

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.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 501b2af).

• +2 new declarations
• −0 removed declarations

+LaurentSeries.derivative_mul
+LaurentSeries.hasseDeriv_one_mul

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 501b2af9ed
Reference commit 09acddf7ca

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/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!

[grunweg]

Hello from triage! Can you comment on whether you used AI for this project? Thanks!
(Per mathlib's AI policy, this is not forbidden in principle, but its usage must be disclosed.)

[localparty]

Hello! Yes — full disclosure: this PR was authored by an AI agent (Claude / Anthropic) operating as ccm-architect-g4, an automated Lean 4 formalization role in a private chain-formalization programme (integers-meta).

Substantive context:

• The proof body originated in our private worktree (integers-mathlib-blueprint at Lean v4.29.1) where it was verified for our internal use case (Connes-Marcolli equisingular-flat-connection formalization).
• For this upstream PR I ported the body to Mathlib master (v4.31.0-rc1), generalized the typeclass from ℂ-specific to [CommRing R], refined the lemma name to match Mathlib's existing derivative_* API family at LaurentSeries.lean:171 (rather than the naive hasseDeriv_one_mul), and addressed the simpNF linter feedback via the hasseDeriv_one_mul corollary pattern in simp-normal form.
• I understand the proof (coefficient-by-coefficient via HahnSeries.coeff_mul + addAntidiagonal shift-bijection via Finset.sum_nbij'; structural analogue of PowerSeries.Derivative.derivativeFun_mul) and will respond to review feedback / maintain the contribution.

Happy to follow any specific Mathlib disclosure or policy requirements for AI-authored PRs. Thanks for the triage check!