Filippo A. E. Nuccio
Filippo A. E. Nuccio
introduce H-spaces and prove basic properties, in particular that every topological group is a H-space and that the path space at a point is a H-space. --- - depends on:...
feat(topology): composition of continuous functions is continuous w.r.t. the compact-open topologies
* Remove the `t2_space` assumption from `exists_compact_between` by generalizing the proof of `exists_compact_superset`, and move it from `topology/separation` to `topology/subset_properties`. * Use it to prove `continuous_map.continuous_prod` in `topology/continuous_map` stating that...
For users coming from other communities, the fact that $\Pi$ types are represented without the symbol $\Pi$, but simply as ```lean (x : α) → β x ``` might be...
Modify the instructions in the naming convention file about `LT` vs `lt` and add a new example. Add a sentence requiring to fork before creating a PR in the readme.md...
Add several properties of the $X$-adic valuation on the ring $K[[X]]$ when $K$ is a field. It depends on #13065. Co-authored-by: María Inés de Frutos-Fernández @mariainesdff
Add two lemmas on the multiplicity of normalized factors in relation to principal ideals and the cardinality of associates. Co-authored-by: María Inés de Frutos-Fernández @mariainesdff --- [](https://gitpod.io/from-referrer/)
Add two lemmas about the element `X` as term of the normalization monoid $k[[X]]$ for a field `k`. Co-authored-by: María Inés de Frutos-Fernández @mariainesdff
Add a lemma showing that composing the comparison maps with a continuous function to a T3 space satisfying some conditions yield the same function. Co-authored with : María Inés de...
Add some properties conneccting the $X$-adic valuation of a Laurent series to the vanishing of its coefficients, together with explicit values of the valuation of some basic Laurent series. Co-authored-by:...
The unique report (as by Apr 28th, 2025) for https://afm.episciences.org/administratepaper/view?id=13987 has been pasted with a full formatting (in particular, new lines for each comment) but once saved the whole formatting...