feat(Algebra): total monoid algebra

[BryceT233]

This PR introduces TotalMonoidAlgebra and TotalAddMonoidAlgebra, which is part of the broader plan on reworking Finsupp, MonoidAlgebra, HahnSeries. PowerSeries.

We mirror the construction in MonoidAlgebra/Defs.lean, but drops the finiteness condition on the support of the elements. In the literature, this construction is called the "large algebra of a monoid" or "total algebra" (see https://en.wikipedia.org/wiki/Total_algebra). When the underlying monoid is finitely supported functions valued in ℕ, this construction corresponds to the multivariate formal power series in the large sense, where arbitrary infinite sums of monomials are permitted.

The algebraic hierarchy in this file is completely identical to that ofMonoidAlgebra/Defs.lean. It builds up the algebraic structure from basic typeclasses like One and SMul, through Mul, NonUnitalNonAssocSemiring, and ultimately to Ring and CommRing. Despite the identical hierarchy, the underlying implementation requires several key departures from MonoidAlgebra:

1. Coefficients are represented using standard functions (M → R) rather than finitely supported functions (M →₀ R). Because of this, this file provides no induction principles or lemmas related to induction principles of Finsupp.

2. The construction uses Pi.single instead of Finsupp.single to represent individual terms. Because of how Pi.single is defined, this imposes a DecidableEq M requirement on many declarations, particularly whenever the identity element is required.

3. To ensure the convolution product is well-defined (i.e., the coefficient sum is finite), we require the underlying monoid to satisfy the Finset.HasMulAntidiagonal M condition. Because of this, proofs concerning multiplication rely heavily on the Finset.sum.

4. When the underlying domain M is a group, the HasMulAntidiagonal condition is essentially equivalent to the group being finite. Furthermore, when M is finite, the total monoid algebra is equivalent to the standard MonoidAlgebra (#Todo). Because it reduces to the standard finite case, this file omits a dedicated group section entirely.

---

• depends on: chore(Algebra/Order/Antidiag): relax an assumption in the definition of HasAntidiagonal #41521

[mathlib-bors]

This pull request is now in draft mode. No active bors state needed cleanup.

While this PR remains draft, bors will ignore commands on this PR. Mark it ready for review before using commands like bors r+ or bors try.

[github-actions]

PR summary 1c123b5e33

Import changes exceeding 2%

%	File
+49.60%	Mathlib.Algebra.Order.Antidiag.Tendsto

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Order.Antidiag.Tendsto	623	932	+309 (+49.60%)

Import changes for all files

Files	Import difference
Mathlib.RingTheory.MvPowerSeries.Restricted	1
Mathlib.Algebra.Order.Antidiag.Tendsto	309
Mathlib.Algebra.TotalMonoidAlgebra.Defs (new file)	661

---

Declarations diff (regex)

+ TotalAddMonoidAlgebra
+ TotalMonoidAlgebra
+ _root_.TotalAddMonoidAlgebra.mul'
+ _root_.TotalMonoidAlgebra.mul'
+ addCommGroup
+ coe_mulAntidiagonal_eq_preimage_singleton
+ coeffAddEquiv
+ coeffEquiv
+ coeffEquiv_apply
+ coeff_add
+ coeff_eq_zero
+ coeff_finsuppSum
+ coeff_inj
+ coeff_injective
+ coeff_mul
+ coeff_mul_single_eq_coeff_mul
+ coeff_mul_single_mul
+ coeff_mul_single_of_forall_mul_ne
+ coeff_mul_single_one
+ coeff_natCast
+ coeff_neg
+ coeff_ofCoeff
+ coeff_ofNat
+ coeff_one_one
+ coeff_single
+ coeff_single_apply
+ coeff_single_mul_eq_mul_coeff
+ coeff_single_mul_mul
+ coeff_single_mul_of_forall_mul_ne
+ coeff_single_one_mul
+ coeff_smul
+ coeff_smul_apply
+ coeff_sub
+ coeff_sum
+ coeff_uniqueRingEquiv_symm
+ coeff_update
+ coeff_zero
+ commRing
+ commSemiring
+ curry
+ curryAddEquiv
+ curryAddEquiv_single
+ curryAddEquiv_symm_single
+ curryRingEquiv
+ curryRingEquiv_single
+ curryRingEquiv_symm_single
+ distribSMul
+ ext
+ finsuppProd_single
+ hasMulAntidiagonal
+ instAddCommMonoid
+ instAddMonoid
+ instInhabited
+ instIsCancelAdd
+ instMul
+ instNontrivial
+ instUnique
+ instance [DecidableEq A] [DecidableEq B] : HasMulAntidiagonal (A × B)
+ instance [Mul A] : Subsingleton (HasMulAntidiagonal A)
+ intCast_def
+ isCentralScalar
+ isLocalHom_singleOneRingHom
+ isScalarTower
+ mulSingle_eq_mulSingle_iff
+ mul_def
+ natCast_def
+ neg_apply
+ nonAssocRing
+ nonAssocSemiring
+ nonUnitalCommRing
+ nonUnitalCommSemiring
+ nonUnitalNonAssocRing
+ nonUnitalNonAssocSemiring
+ nonUnitalRing
+ nonUnitalSemiring
+ of'
+ of'_apply
+ of'_commute
+ of'_eq_of
+ ofCoeff_add
+ ofCoeff_coeff
+ ofCoeff_eq_zero
+ ofCoeff_finsuppSum
+ ofCoeff_inj
+ ofCoeff_injective
+ ofCoeff_neg
+ ofCoeff_single
+ ofCoeff_smul
+ ofCoeff_sub
+ ofCoeff_sum
+ ofCoeff_update
+ ofCoeff_zero
+ ofNat_def
+ of_apply
+ of_commute
+ one
+ one_def
+ prod_single
+ ring
+ semiring
+ single
+ singleAddMonoidHom
+ singleOneRingHom
+ single_add
+ single_commute
+ single_commute_single
+ single_eq_zero
+ single_inj
+ single_left_inj
+ single_left_injective
+ single_mul_single
+ single_ne_zero
+ single_neg
+ single_one_comm
+ single_pow
+ single_right_inj
+ single_right_injective
+ single_sub
+ single_zero
+ smulCommClass
+ smulZeroClass
+ smul_single
+ smul_single'
+ tendstoCofinite_mul
+ uniqueRingEquiv
+ uniqueRingEquiv_symm_apply
+ update
+ «exists»
+ «forall»
++ of
++ ofMagma
++ of_injective
++ singleHom
- instance [Monoid A] : Subsingleton (HasMulAntidiagonal A)

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 1c123b5).

• +306 new declarations
• −0 removed declarations

(showing first 200 of 306 lines)

+AddEquiv.curry
+AddEquiv.curry_apply
+AddEquiv.curry_symm_apply
+Filter.TendstoCofinite.hasAntidiagonal
+Filter.TendstoCofinite.hasMulAntidiagonal
+Finset.HasAntidiagonal.coe_antidiagonal_eq_preimage_singleton
+Finset.HasAntidiagonal.instSumOfDecidableEq
+Finset.HasAntidiagonal.tendstoCofinite_add
+Finset.HasMulAntidiagonal.coe_mulAntidiagonal_eq_preimage_singleton
+Finset.HasMulAntidiagonal.instProdOfDecidableEq
+Finset.HasMulAntidiagonal.tendstoCofinite_mul
+MulEquiv.curry
+MulEquiv.curry_apply
+MulEquiv.curry_symm_apply
+Pi.mulSingle.hcongr_6
+Pi.mulSingle_eq_mulSingle_iff
+Pi.single_eq_single_iff
+TotalAddMonoidAlgebra
+TotalAddMonoidAlgebra.addCommGroup
+TotalAddMonoidAlgebra.casesOn
+TotalAddMonoidAlgebra.coeff
+TotalAddMonoidAlgebra.coeffAddEquiv
+TotalAddMonoidAlgebra.coeffAddEquiv_apply
+TotalAddMonoidAlgebra.coeffAddEquiv_symm_apply
+TotalAddMonoidAlgebra.coeffEquiv
+TotalAddMonoidAlgebra.coeffEquiv_symm_apply
+TotalAddMonoidAlgebra.coeff_add
+TotalAddMonoidAlgebra.coeff_eq_zero
+TotalAddMonoidAlgebra.coeff_finsuppSum
+TotalAddMonoidAlgebra.coeff_inj
+TotalAddMonoidAlgebra.coeff_injective
+TotalAddMonoidAlgebra.coeff_mul
+TotalAddMonoidAlgebra.coeff_mul_single_add
+TotalAddMonoidAlgebra.coeff_mul_single_eq_coeff_mul
+TotalAddMonoidAlgebra.coeff_mul_single_of_forall_add_ne
+TotalAddMonoidAlgebra.coeff_mul_single_zero
+TotalAddMonoidAlgebra.coeff_natCast
+TotalAddMonoidAlgebra.coeff_neg
+TotalAddMonoidAlgebra.coeff_ofCoeff
+TotalAddMonoidAlgebra.coeff_ofNat
+TotalAddMonoidAlgebra.coeff_single
+TotalAddMonoidAlgebra.coeff_single_apply
+TotalAddMonoidAlgebra.coeff_single_mul_add
+TotalAddMonoidAlgebra.coeff_single_mul_eq_mul_coeff
+TotalAddMonoidAlgebra.coeff_single_mul_of_forall_add_ne
+TotalAddMonoidAlgebra.coeff_single_zero_mul
+TotalAddMonoidAlgebra.coeff_smul
+TotalAddMonoidAlgebra.coeff_smul_apply
+TotalAddMonoidAlgebra.coeff_sub
+TotalAddMonoidAlgebra.coeff_sum
+TotalAddMonoidAlgebra.coeff_uniqueRingEquiv_symm
+TotalAddMonoidAlgebra.coeff_update
+TotalAddMonoidAlgebra.coeff_zero
+TotalAddMonoidAlgebra.coeff_zero_zero
+TotalAddMonoidAlgebra.commRing
+TotalAddMonoidAlgebra.commSemiring
+TotalAddMonoidAlgebra.ctorIdx
+TotalAddMonoidAlgebra.curryAddEquiv
+TotalAddMonoidAlgebra.curryAddEquiv_single
+TotalAddMonoidAlgebra.curryAddEquiv_symm_single
+TotalAddMonoidAlgebra.curryRingEquiv
+TotalAddMonoidAlgebra.curryRingEquiv_single
+TotalAddMonoidAlgebra.curryRingEquiv_symm_single
+TotalAddMonoidAlgebra.delabOfCoeff
+TotalAddMonoidAlgebra.distribSMul
+TotalAddMonoidAlgebra.exists
+TotalAddMonoidAlgebra.ext
+TotalAddMonoidAlgebra.ext_iff
+TotalAddMonoidAlgebra.finsuppProd_single
+TotalAddMonoidAlgebra.forall
+TotalAddMonoidAlgebra.instAddCommMonoid
+TotalAddMonoidAlgebra.instAddMonoid
+TotalAddMonoidAlgebra.instInhabited
+TotalAddMonoidAlgebra.instIsCancelAdd
+TotalAddMonoidAlgebra.instMul
+TotalAddMonoidAlgebra.instNontrivial
+TotalAddMonoidAlgebra.instUnique
+TotalAddMonoidAlgebra.intCast_def
+TotalAddMonoidAlgebra.isCentralScalar
+TotalAddMonoidAlgebra.isLocalHom_singleZeroRingHom
+TotalAddMonoidAlgebra.isScalarTower
+TotalAddMonoidAlgebra.mul'
+TotalAddMonoidAlgebra.mul_def
+TotalAddMonoidAlgebra.natCast_def
+TotalAddMonoidAlgebra.noConfusion
+TotalAddMonoidAlgebra.noConfusionType
+TotalAddMonoidAlgebra.nonAssocRing
+TotalAddMonoidAlgebra.nonAssocSemiring
+TotalAddMonoidAlgebra.nonUnitalCommRing
+TotalAddMonoidAlgebra.nonUnitalCommSemiring
+TotalAddMonoidAlgebra.nonUnitalNonAssocRing
+TotalAddMonoidAlgebra.nonUnitalNonAssocSemiring
+TotalAddMonoidAlgebra.nonUnitalRing
+TotalAddMonoidAlgebra.nonUnitalSemiring
+TotalAddMonoidAlgebra.of
+TotalAddMonoidAlgebra.of'
+TotalAddMonoidAlgebra.of'_apply
+TotalAddMonoidAlgebra.of'_commute
+TotalAddMonoidAlgebra.of'_eq_of
+TotalAddMonoidAlgebra.ofCoeff
+TotalAddMonoidAlgebra.ofCoeff.inj
+TotalAddMonoidAlgebra.ofCoeff.injEq
+TotalAddMonoidAlgebra.ofCoeff.noConfusion
+TotalAddMonoidAlgebra.ofCoeff.sizeOf_spec
+TotalAddMonoidAlgebra.ofCoeff_add
+TotalAddMonoidAlgebra.ofCoeff_coeff
+TotalAddMonoidAlgebra.ofCoeff_eq_zero
+TotalAddMonoidAlgebra.ofCoeff_finsuppSum
+TotalAddMonoidAlgebra.ofCoeff_inj
+TotalAddMonoidAlgebra.ofCoeff_injective
+TotalAddMonoidAlgebra.ofCoeff_neg
+TotalAddMonoidAlgebra.ofCoeff_single
+TotalAddMonoidAlgebra.ofCoeff_smul
+TotalAddMonoidAlgebra.ofCoeff_sub
+TotalAddMonoidAlgebra.ofCoeff_sum
+TotalAddMonoidAlgebra.ofCoeff_update
+TotalAddMonoidAlgebra.ofCoeff_zero
+TotalAddMonoidAlgebra.ofMagma
+TotalAddMonoidAlgebra.ofMagma_apply
+TotalAddMonoidAlgebra.ofNat_def
+TotalAddMonoidAlgebra.of_apply
+TotalAddMonoidAlgebra.of_injective
+TotalAddMonoidAlgebra.one_def
+TotalAddMonoidAlgebra.prod_single
+TotalAddMonoidAlgebra.rec
+TotalAddMonoidAlgebra.recOn
+TotalAddMonoidAlgebra.ring
+TotalAddMonoidAlgebra.semiring
+TotalAddMonoidAlgebra.single
+TotalAddMonoidAlgebra.singleAddAddMonoidHom
+TotalAddMonoidAlgebra.singleAddAddMonoidHom_apply
+TotalAddMonoidAlgebra.singleHom
+TotalAddMonoidAlgebra.singleHom_apply
+TotalAddMonoidAlgebra.singleZeroRingHom
+TotalAddMonoidAlgebra.singleZeroRingHom_apply
+TotalAddMonoidAlgebra.single_add
+TotalAddMonoidAlgebra.single_commute
+TotalAddMonoidAlgebra.single_commute_single
+TotalAddMonoidAlgebra.single_eq_zero
+TotalAddMonoidAlgebra.single_inj
+TotalAddMonoidAlgebra.single_left_inj
+TotalAddMonoidAlgebra.single_left_injective
+TotalAddMonoidAlgebra.single_mul_single
+TotalAddMonoidAlgebra.single_ne_zero
+TotalAddMonoidAlgebra.single_neg
+TotalAddMonoidAlgebra.single_pow
+TotalAddMonoidAlgebra.single_right_inj
+TotalAddMonoidAlgebra.single_right_injective
+TotalAddMonoidAlgebra.single_sub
+TotalAddMonoidAlgebra.single_zero
+TotalAddMonoidAlgebra.single_zero_comm
+TotalAddMonoidAlgebra.smulCommClass
+TotalAddMonoidAlgebra.smulZeroClass
+TotalAddMonoidAlgebra.smul_single
+TotalAddMonoidAlgebra.smul_single'
+TotalAddMonoidAlgebra.unexpander
+TotalAddMonoidAlgebra.uniqueRingEquiv
+TotalAddMonoidAlgebra.uniqueRingEquiv_apply
+TotalAddMonoidAlgebra.uniqueRingEquiv_symm_apply
+TotalAddMonoidAlgebra.update
+TotalAddMonoidAlgebra.zero
+TotalAddMonoidAlgebra.«term__⟦_⟧»
+TotalMonoidAlgebra
+TotalMonoidAlgebra.addCommGroup
+TotalMonoidAlgebra.casesOn
+TotalMonoidAlgebra.coeff
+TotalMonoidAlgebra.coeffAddEquiv
+TotalMonoidAlgebra.coeffAddEquiv_apply
+TotalMonoidAlgebra.coeffAddEquiv_symm_apply
+TotalMonoidAlgebra.coeffEquiv
+TotalMonoidAlgebra.coeffEquiv_apply
+TotalMonoidAlgebra.coeffEquiv_symm_apply
+TotalMonoidAlgebra.coeff_add
+TotalMonoidAlgebra.coeff_eq_zero
+TotalMonoidAlgebra.coeff_finsuppSum
+TotalMonoidAlgebra.coeff_inj
+TotalMonoidAlgebra.coeff_injective
+TotalMonoidAlgebra.coeff_mul
+TotalMonoidAlgebra.coeff_mul_single_eq_coeff_mul
+TotalMonoidAlgebra.coeff_mul_single_mul
+TotalMonoidAlgebra.coeff_mul_single_of_forall_mul_ne
+TotalMonoidAlgebra.coeff_mul_single_one
+TotalMonoidAlgebra.coeff_natCast
+TotalMonoidAlgebra.coeff_neg
+TotalMonoidAlgebra.coeff_ofCoeff
+TotalMonoidAlgebra.coeff_ofNat
+TotalMonoidAlgebra.coeff_one_one
+TotalMonoidAlgebra.coeff_single
+TotalMonoidAlgebra.coeff_single_apply
+TotalMonoidAlgebra.coeff_single_mul_eq_mul_coeff
+TotalMonoidAlgebra.coeff_single_mul_mul
+TotalMonoidAlgebra.coeff_single_mul_of_forall_mul_ne
+TotalMonoidAlgebra.coeff_single_one_mul
+TotalMonoidAlgebra.coeff_smul
+TotalMonoidAlgebra.coeff_smul_apply
+TotalMonoidAlgebra.coeff_sub
+TotalMonoidAlgebra.coeff_sum
+TotalMonoidAlgebra.coeff_uniqueRingEquiv_symm
+TotalMonoidAlgebra.coeff_update
+TotalMonoidAlgebra.coeff_zero

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 1c123b5e33
Reference commit a33a5ccd63

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 Needs Formatting

Please update the title to match our commit style conventions.

Errors from script:

labels are []
error: the PR title should be of the form
  kind: subject
or
  kind(scope): subject
Allowed values for `kind` are [feat, chore, perf, refactor, style, fix, doc, test, ci]

Details on the required title format

The title should fit the following format:

<kind>(<optional-scope>): <subject>

<kind> is:

• feat (feature)
• fix (bug fix)
• doc (documentation)
• style (formatting, missing semicolons, ...)
• refactor
• test (when adding missing tests)
• chore (maintain)
• perf (performance improvement, optimization, ...)
• ci (changes to continuous integration, repo automation, ...)

<optional-scope> is a name of module or a directory which contains changed modules.
This is not necessary to include, but may be useful if the <subject> is insufficient.
The Mathlib directory prefix is always omitted.
For instance, it could be

• Data/Nat/Basic
• Algebra/Group/Defs
• Topology/Constructions

<subject> has the following constraints:

• do not capitalize the first letter
• no dot(.) at the end
• use imperative, present tense: "change" not "changed" nor "changes"

[mathlib-dependent-issues]

This PR/issue depends on:

• chore(Algebra/Order/Antidiag): relax an assumption in the definition of HasAntidiagonal #41521
  By Dependent Issues (🤖). Happy coding!