Theorem multipliable_of_exists_eq_zero

Modification history

2025-04-08 15:48

Mathlib/Topology/Algebra/InfiniteSum/Basic.lean

feat(Topology/Algebra/InfiniteSum): lemmas about tprods in a GroupWithZero (#23803) …

Added multipliable_of_exists_eq_zero View on Github →