is_closed.smul for fields

Stream: Is there code for X?

[Moritz Doll]

Given a nonzero element a in a field I want to show that a • U is closed provided U is closed and we have all the necessary typeclasses.

variables {𝕜 E : Type*}

variables [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E]
  [has_continuous_smul 𝕜 E]

lemma test {U : set E} {a : 𝕜} (hU : is_closed U) (ha : a ≠ 0) : is_closed (a • U) := sorry

Using is_closed.smul complains (rightly so) that 𝕜 is no group and I haven't found the path to turn all nonzero elements into a group. I only found group_with_zero, but I have no clue whether that helps.

[Kevin Buzzard]

Division by a is continuous, that should get you through. (I would have tried myself but you didn't post a mwe ;-) )

[Yaël Dillies]

Use docs#units.mk0

[Yury G. Kudryashov]

Please add it right after docs#is_open.smul₀.

[Yury G. Kudryashov]

https://leanprover-community.github.io/mathlib_docs/topology/algebra/const_mul_action.html#is_open.smul%E2%82%80

[Yury G. Kudryashov]

(together with is_closed_map_smul₀)

[Moritz Doll]

There is already docs#is_closed_map_smul_of_ne_zero so I only have to add one lemma. The naming is a bit inconsistent, though

[Moritz Doll]

#12747

[Damiano Testa]

Maybe I am missing something, but is the assumption $a \ne 0$ really necessary? I can see that the proof goes via a homeomorphism, which rightly requires it, but this statement should not need that assumption, right?

[Moritz Doll]

The set $\{0\}$ is not necessarily closed. If it is Hausdorff (or T1), then you are correct:
https://leanprover-community.github.io/mathlib_docs/topology/algebra/const_mul_action.html#is_closed_map_smul%E2%82%80

[Moritz Doll]

thanks for mentioning it. I put a version for T1 in my PR.

[Eric Wieser]

The naming is definitely a mess there