Abstract Hecke ring: the Ring (𝕋 P ℤ) instance

[CBirkbeck]

Abstract Hecke ring: the Ring instance

A focused PR proving that the abstract Hecke ring is a Ring — and nothing more. Following Shimura, Introduction to the Arithmetic Theory of Automorphic Functions, Ch. 3.

New LeanBridge/ForMathlib/AbstractHeckeRing/ with exactly the files needed for Ring (𝕋 P ℤ):

• Basic — the Hecke pair HeckePair, the double-coset quotient HeckeCoset, and the Hecke ring type 𝕋;
• Multiplication — the convolution product via Shimura's integer multiplicities;
• Module — the module action of 𝕋 on the left-coset module (used by the associativity argument);
• Associativity — associativity of the convolution;
• Ring — the resulting Ring (𝕋 P ℤ) instance (NonUnitalSemiring → NonAssocSemiring → Semiring → NonAssocRing → Ring).

Scope (deliberately minimal)

• Only the ring structure. Commutativity (from an anti-involution), the degree map, and the remaining API are left to follow-up PRs.
• Module is included because the associativity proof goes through the module-action scalar tower (Ring → Associativity → Module → Multiplication → Basic); it is a proof dependency, not extra scope.
• The coefficient ring is ℤ. Generalising the ring/module layer to an arbitrary commutative ring R is a separate follow-up.

Verification

✅ lake build clean against pinned mathlib v4.31.0 (1830 jobs). No sorry / axiom. Ported from the AINTLIB project (projects/LeanModularForms/.../AbstractHeckeRing).

Part of #75. (Supersedes the everything-at-once #77 for the ring part; commutativity/module-API/degree will land as their own PRs.)