Measurability of units multiplication

Stream: Is there code for X?

[Yaël Dillies]

Is this true?

import measure_theory.group.arithmetic

variables {α : Type*} [measurable_space α] [monoid α] [has_measurable_mul₂ α]

instance : has_measurable_mul₂ αˣ := sorry

[Kevin Buzzard]

Is this your homework? :-)

[Yaël Dillies]

I wish it was, but Probability & Measure is a Michaelmas course! I need the above to golf #17570 a bit further.

[Sebastien Gouezel]

What measurable structure are you putting on the units? In the topological case, the good topological structure is arguably not the induced topology, but the one that also takes into account the topology for the inverse. One should probably do the same for the measurable structure, and then it's very unlikely that the assumption you have is sufficient for your instance.

[Yaël Dillies]

There's docs#units.measurable_space, which is the pullback under αˣ → α × α.