Theorem Multipliable.hasFiniteMulSupport_of_discreteTopology

Modification history

2026-03-04 08:58
Mathlib/Topology/Algebra/InfiniteSum/Group.lean
chore: adapt names after #34658 (#36080) …
Added Multipliable.hasFiniteMulSupport_of_discreteTopologyView on Github →