feat: Lindemann-Weierstrass Theorem

[astrainfinita]

---

There's still a lot of work to be done before it gets into mathlib.

• [x] depends on: #6593
• [x] depends on: #6719
• [x] depends on: #6723
• [x] depends on: #6740
• [x] depends on: #7274
• [x] depends on: #8807
• [x] depends on: #12191
• [x] depends on: #12764
• [x] depends on: #16259
• [x] depends on: #16262
• [x] depends on: #16886
• [x] depends on: #16898
• [x] depends on: #16923
• [x] depends on: #16933
• [x] depends on: #17119
• [x] depends on: #17893
• [x] depends on: #17894
• [x] depends on: #17896