Commit 2024-09-20 16:59 1912fa59

chore: move things around in the Analytic folder (#16972) We move some things in the Analytic folder, particularly in and out of Basic. Notably

• The fact that the addition and subtraction are analytic is moved from Basic to Constructions, where there are already the same facts for multiplication and scalar multiplication
• Congruence lemmas are moved from Within to Basic
• Uniqueness of power series is moved from Basic to the (already existing file!) Uniqueness
• Order of imports is swapped between Calculus.FDeriv.Analytic and Analytic.Within. We also add a few docstrings to the files to show their structure. This gives a more principled hierarchy, better suited to the addition of future lemmas. This PR is just moving things around, no statement has been added or removed.