Oliver Nash comments

Results 30 comments of


                                            Oliver Nash

feat(analysis/convex/cone): dual_of_dual_eq_self

Thanks! Please apply my suggestions and then feel free to merge. bors d+

feat(analysis/convex/cone): dual_of_dual_eq_self

Please also update the PR description: it seems to be out of date.

refactor(analysis/inner_product_space): rename `is_self_adjoint` to `is_symmetric` and add `is_self_adjoint`

bors d=j-loreaux

feat(analysis/locally_convex): the topology of a locally convex space is generated by seminorms

bors d=ADedecker

feat(topology): composition of continuous functions is continuous w.r.t. the compact-open topologies

Thanks! bors merge

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

Thanks! bors merge

feat(topology/algebra/uniform_ring): ring completions and algebra structures

I suggest addressing @jcommelin 's remark by adding a sentence along the lines of: ``` TODO Generalise the results here from the concrete `completion` to any `abstract_completion`. ``` to the...

feat(analysis/convolution): prove associativity under more convenient assumptions

Thanks! bors merge

feat(ring_theory/dedekind_domain/finite_adele_ring): add finite_adele_ring

@riccardobrasca is right and that we should be using the `algebra` typeclass more here. Even before we get to the adèles I think there are various little gaps to fill....

feat(ring_theory/dedekind_domain/finite_adele_ring): add finite_adele_ring

Hmm, even the following seems to be missing: ```lean import topology.algebra.uniform_ring import algebra.algebra.basic noncomputable theory variables (A : Type*) [comm_ring A] [uniform_space A] [uniform_add_group A] variables [topological_ring A] [uniform_add_group A]...