Commit 2021-03-30 14:01 e1f66f1a

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.