chore(Algebra/Order/Antidiag): relax an assumption in the definition of HasAntidiagonal

[BryceT233]

This PR relaxes the typeclass requirement for HasAntidiagonal from AddMonoid A to Add A, which is useful for defining multiplications in TotalMonoidAlgebra(#41472).

---

[github-actions]

PR summary 97fd7385b0

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ instance [Mul A] : Subsingleton (HasMulAntidiagonal A)
- 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 97fd738).

• +0 new declarations
• −0 removed declarations

No declaration differences.

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 97fd7385b0
Reference commit 80ffd59621

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

[eric-wieser]

Can you elaborate on what makes this useful?

Also, please generalize the theorems further down the file where possible; there's little value in generalizing only the definition.

[BryceT233]

Can you elaborate on what makes this useful?

Also, please generalize the theorems further down the file where possible; there's little value in generalizing only the definition.

Apologies for the lack of detail in the initial description. I'm currently constructing TotalMonoidAlgebra/Defs.lean, which mirrors the structure of MonoidAlgebra/Defs.lean. Over there, the algebraic hierarchy is built incrementally: we first obtain a NonUnitalNonAssocSemiring from a mere magma Mul M, and then upgrade the structures assuming Semigroup M, Monoid M, etc. To define multiplication in TotalMonoidAlgebra at this base level, we only require the finiteness of the antidiagonal. The AddMonoid requirement in Finset.HasAntidiagonal is therefore too strong for my purpose.

I also considered an alternative approach: keeping HasAntidiagonal as is and just using Add M along with TendstoCofinite (fun (p : M × M) ↦ p.1 + p.2). I wasn't completely sure which way is better though.

[eric-wieser]

That justification seems good enough to me, but please generalize some lemmas too!