Commit 2025-12-19 21:09 6335ae01

refactor(Data/Nat/Choose): Merge Basic.lean and Mul.lean (#32901) Previously, Mul.lean contained two very basic identities about polynomial coefficients and was its own file due to the use of ring. I replaced the usage of ring via some rewrites (not too bad), making it possible to merge Mul.lean into Basic.lean (which is appropriate content-wise). Sidenote: The list of authors is now over 100 characters long. I did not find another file where this is the case, so I don''t know what is the standard format in this case.