mathlib3

3782acf1 - feat(topology/algebra/*): Criterion to ensure topological monoids and groups (#5284)

feat(topology/algebra/*): Criterion to ensure topological monoids and groups (#5284) This is old stuff from the perfectoid project that was never PRed and is useful for the liquid tensor experiment.