mathlib

e1f66f1a - feat(topology/algebra/group_with_zero): continuity of exponentiation to an integer power (`fpow`) (#6937)

feat(topology/algebra/group_with_zero): continuity of exponentiation to an integer power (`fpow`) (#6937) In a topological group-with-zero (more precisely, in a space with `has_continuous_inv'` and `has_continuous_mul`), the `k`-th power function is continuous for integer `k`, with the possible exception of at 0.