Commit 2026-01-07 19:24 667d6f2c

chore(Topology/Covering): adjust some statements (#33721) The new statements are defeq to the old ones but shorter (when written in full with namespaces) and require less imports. Also the new statements involve additivized decls, while the original DistribMulAction.toAddMonoidHom doesn't have an appropriate multiplicative version (MulDistribMulAction.toMonoidHom can't be automatically additivized, and we want Pow instead of SMul for the multiplicative version). Also replaces n ≠ 0 by [NeZero n]. See also #33724.