mathlib

6b3b567f - chore(topology/algebra/group_with_zero): fix docstring for has_continuous_inv0 (#12653)