Vincent Beffara
Vincent Beffara
Thanks for all the comments and changes! I will need some time to process all the `mk_pi` stuff, but just to answer 2 questions that came up related to a...
In `filter.tendsto.eventually_ne` as it is now, the linter says that `α` does not have to be a `topological_space`, which makes sense. I just added a microscopic commit to appease the...
The PR has gone a little stale, I just merged master and it doesn't build anymore (same issue as in #16074), let's fix it
See #12 I believe it solves that exact problem
I hadn't thought about generalizations (I should have known by now ;->) but definitely some are possible. For `E \to \C`, most would go through as soon as `[proper_space E]`...
This is going to work for the generalization: ```lean example {E : Type*} [normed_add_comm_group E] [normed_space ℂ E] {z₀ : E} {g : E → ℂ} (hg : analytic_at ℂ...
OK, so I extended both `analytic_at.eventually_constant_or_nhds_le_map_nhds` and `analytic_on.is_constant_or_is_open` to the `E → ℂ` case, and I believe I addressed all the other comments.
Docstrings added. bors r+