Oliver Nash

Also update doc string for `topological_group.to_uniform_space`. cc @ADedecker --- [](https://gitpod.io/from-referrer/)

feat(analysis/normed_space/basic): change `homeomorph_unit_ball` to make it obviously smooth

2

Formalized as part of the Sphere Eversion project. --- [](https://gitpod.io/from-referrer/)

feat(*): add various order-related lemmas

3

These all came up while preparing to introduce the definition of ergodic maps but it seems better to PR them separately. --- [](https://gitpod.io/from-referrer/)

--- See also comments [on Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/ideals.20in.20non-comm.20rings/near/284039475) [](https://gitpod.io/from-referrer/)

We have a diamond of complete boolean algebras on sets: ```lean import data.set.lattice variables {α : Type*} -- Succeeds example : @set.boolean_algebra α = pi.boolean_algebra := rfl -- Fails example...

--- Split out from #12937 (suggestions there applied here) [](https://gitpod.io/from-referrer/)

feat: Lie algebra root spaces are 1-dimensional

1

over a field of characteristic zero, when the Killing form is non-singular --- - [ ] depends on: #13076 [](https://gitpod.io/from-referrer/)

A semisimple Lie algebra is a direct sum of simple Lie algebras

4

In characteristic zero, a [semisimple Lie algebra](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Lie/Semisimple.html#LieAlgebra.IsSemisimple) is a direct sum of [simple Lie algebra](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Lie/Semisimple.html#LieAlgebra.IsSimple)s. We should add this result to Mathlib. I think the most useful statement of this...

Linter `doc_blame` generates unwanted warning when using `old_structure_cmd`

2

The following snippet triggers the "missing doc string" complaint from the linter: ```lean set_option old_structure_cmd true /-- Foo structure -/ structure foo := (x : ℕ) /-- Bar structure -/...