Units of product of topological rings

Stream: Is there code for X?

[María Inés de Frutos Fernández]

If R and S are rings then the group of units of R × S is isomorphic to units R × units S. Moreover, if R and S are topological rings, then this is an isomorphism of topological groups. Do we have this in mathlib? I.e., do we have something equivalent to

import topology.algebra.ring

variables (R S : Type*) [ring R]  [ring S]

def prod_units.mul_equiv : mul_equiv (units (R × S)) ((units R) × (units S)) :=
sorry

variables [ topological_space R] [topological_ring R] [topological_space S] [topological_ring S]

def prod_units.homeo : homeomorph (units (R × S)) ((units R) × (units S)) :=
{ continuous_to_fun  := sorry,
  continuous_inv_fun := sorry,
  ..prod_units.mul_equiv R S }

Otherwise I have a version of this I could PR.

[Yury G. Kudryashov]

Note that this should be true for monoids, not necessary rings.

[Yury G. Kudryashov]

We have docs#mul_equiv.prod_units

[Yury G. Kudryashov]

The homeomorph version is not here, and it should go to topology.algebra.monoid.

[María Inés de Frutos Fernández]

Thanks! I'll adapt my homeomorph proof using mul_equiv.prod_units (and monoids) and PR it.

[María Inés de Frutos Fernández]

I think this should go to topology.algebra.group.