mathlib

mathlib copied to clipboard

feat(algebra/order/complete.field): add real.ring_hom_eq_id

1

Proves that there are no nontrivial ring homomorphism from ℝ to ℝ. This is motivated by a remark of K. Buzzard (see https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Continuous.20complex.20ring.20hom/near/293264751). It looks like it should be a...

xroblot

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

ocfnash

feat(topology/uniform_space/uniform_convergence_topology): continuity of [pre,post]composition, and other topological properties

1

We refactor a bit the beginning of the file to define a lower adjoint to the operation sending a filter on `β × β` to the corresponding "filter of uniform...

ADedecker

feat(analysis/inner_product_space/l2_space): the family of subspaces spanned by finitely many elements of a Hilbert basis has dense supremum

2

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

ADedecker

feat(analysis/convex/topology): minimize import

3

Importing `analysis/normed_space/finite_dimension` was problematic for defining the strong operator topology because this needs quite a few facts about convexity but it has to be defined before `continuous_linear_map.has_op_norm`. --- [![Open in...

ADedecker

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

ADedecker

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/)

ocfnash

The possibilities are `set.univ, U, Uᶜ, ∅`, This lemma is from LTE. --- [](https://gitpod.io/from-referrer/)

adomani

feat(analysis/seminorm): Group seminorms

1

Multiplicativize the existing `add_group_seminorm` material. --- [](https://gitpod.io/from-referrer/)

YaelDillies

feat(order/conditionally_complete_lattice): add `with_top.supr_coe_eq_top` and `with_top.supr_coe_lt_top`

1

--- golfing welcome if you feel the urge. [](https://gitpod.io/from-referrer/)

j-loreaux