feat: Lindemann-Weierstrass Theorem

[FR-vdash-bot]

---

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

• depends on: [Merged by Bors] - feat(MvPolynomial/Symmetric): the fundamental theorem #6593
• depends on: [Merged by Bors] - feat: add some lemmas about Finsupp.indicator #6719
• depends on: [Merged by Bors] - feat(UniqueProds + NoZeroDivisors): AddMonoidAlgebra instances #6723
• depends on: [Merged by Bors] - feat: roots in an algebra #6740
• depends on: [Merged by Bors] - feat: some theorems about iterated polynomial derivatives #7274
• depends on: [Merged by Bors] - feat: add smul_prod lemmas #8807
• depends on: [Merged by Bors] - feat: FloorRing.exists_prime_mul_pow_div_factorial_lt_one #12191
• depends on: [Merged by Bors] - feat: minor API lemmas for (Add)MonoidAlgebra.mapDomainAlgHom #12764
• depends on: [Merged by Bors] - feat: add Complex.isIntegral_{int,rat}_I #16259
• depends on: [Merged by Bors] - feat: add expMonoidHom_apply simp lemmas #16262
• depends on: [Merged by Bors] - feat: sum of iterated derivatives #16886
• depends on: [Merged by Bors] - feat: add AlgEquiv.symm_apply_eq #16898
• depends on: [Merged by Bors] - feat: IntermediateField.adjoinRootEquivAdjoin_symm_apply_gen #16923
• depends on: [Merged by Bors] - feat: some lemmas about polynomial roots #16933
• depends on: [Merged by Bors] - feat: FloorSemiring.tendsto_pow_div_factorial #17119
• depends on: [Merged by Bors] - feat: Algebra.IsAlgebraic.tower_bot #17893
• depends on: [Merged by Bors] - feat: the algebraic closure of an algebraic k-algebra is an algebraic closure of k #17894
• depends on: [Merged by Bors] - feat: Multiset.pow_smul_esymm #17896

[alreadydone]

This file should be easy to PR separately.

In general I think these Equivs should be obtained by combining both directions (RingHoms in this case). We should show that AddMonoidAlgebra · G is a functor (prove the comp and id lemmas) and deduce that both directions are inverse to each other.

Some assumptions might be able to be generalized, e.g. here [AddZeroClass G] should work.

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(MvPolynomial/Symmetric): the fundamental theorem #6593
• [Merged by Bors] - feat: add some lemmas about Finsupp.indicator #6719
• [Merged by Bors] - feat(UniqueProds + NoZeroDivisors): AddMonoidAlgebra instances #6723
• [Merged by Bors] - feat: roots in an algebra #6740
• [Merged by Bors] - feat: some theorems about iterated polynomial derivatives #7274
• [Merged by Bors] - feat: add smul_prod lemmas #8807
• [Merged by Bors] - feat: FloorRing.exists_prime_mul_pow_div_factorial_lt_one #12191
• [Merged by Bors] - feat: minor API lemmas for (Add)MonoidAlgebra.mapDomainAlgHom #12764
• [Merged by Bors] - feat: add Complex.isIntegral_{int,rat}_I #16259
• [Merged by Bors] - feat: add expMonoidHom_apply simp lemmas #16262
• [Merged by Bors] - feat: sum of iterated derivatives #16886
• [Merged by Bors] - feat: add AlgEquiv.symm_apply_eq #16898
• [Merged by Bors] - feat: IntermediateField.adjoinRootEquivAdjoin_symm_apply_gen #16923
• [Merged by Bors] - feat: some lemmas about polynomial roots #16933
• [Merged by Bors] - feat: FloorSemiring.tendsto_pow_div_factorial #17119
• [Merged by Bors] - feat: Algebra.IsAlgebraic.tower_bot #17893
• [Merged by Bors] - feat: the algebraic closure of an algebraic k-algebra is an algebraic closure of k #17894
• [Merged by Bors] - feat: Multiset.pow_smul_esymm #17896
  By Dependent Issues (🤖). Happy coding!