Theorem multipliable_of_hasFiniteMulSupport

Modification history

2026-03-03 17:54

Mathlib/Topology/Algebra/InfiniteSum/Basic.lean

feat(Algebra/Group/FiniteSupport): add HasFinite(Mul)Support and API (#34658) …

Added multipliable_of_hasFiniteMulSupport View on Github →