Ruben Van de Velde

feat(analysis/transcendental): e is transcendental

1

--- #3884, second attempt. [](https://gitpod.io/from-referrer/)

Co-authored-by: Jujian Zhang --- Rewrite of a result from #15954. [](https://gitpod.io/from-referrer/)

Ref: #13776. --- [](https://gitpod.io/from-referrer/)

iterated_deriv.lean was not used anywhere, and derivative.lean already had independent variants of several of the lemmas there, without the `iterated_deriv` indirecion. It seems better to consolidate these results. --- I...

--- [](https://gitpod.io/from-referrer/)

chore: remove Complex/RCLike bit0/1 lemmas

2

These were interesting when they worked on number literals, which is no longer the case in lean4. --- [](https://gitpod.io/from-referrer/)

This was previously about LinearOrderedRing, which is strictly stronger. The new assumptions match sq_nonneg. --- [](https://gitpod.io/from-referrer/)

feat: apply dupNamespace linter to instances

4

This caught 14 bugs with no false positives over in https://github.com/leanprover-community/mathlib4/pull/10899

rcases doesn't seem to support ?_ placeholders

1

```lean import Std.Tactic.RCases theorem aux (h : 0 < 2) : ∃ n : Nat, n = 2 := ⟨2, rfl⟩ example : True := by rcases aux ?_ with...

chore: split order synonym instances for GroupWithZero into their own file

3

This is consistent with the `Group` file, and drops the dependency on `Mathlib.Order` entirely. --- - [x] depends on: #13008 - [x] depends on: #13033 [](https://gitpod.io/from-referrer/)