StronglyMeaurable.div₀

Stream: Is there code for X?

[Yongxi Lin (Aaron)]

We don't have a version of StronglyMeasurable.div for GroupWithZero right? and similarly for AEStronglyMeasurable.div

[Thomas Zhu]

The docstring for docs#ContinuousDiv says "Lemmas using this class have primes. The unprimed version is for GroupWithZero." so perhaps the correct naming would be StronglyMeasurable.div' for Group and StronglyMeasurable.div for GroupWithZero