Commit 2025-04-08 15:48 e1fdf0d0
View on Github →feat(Topology/Algebra/InfiniteSum): lemmas about tprods in a GroupWithZero (#23803)
Show that a sequence with a zero term is always multipliable, and a congruence lemma for Multipliable for eventually-equal sequences. (We have Multipliable.congr_cofinite but that requires the target to be a group under multiplication, which is never satisfied for the underlying multiplicative monoid of a ring; so this new lemma is useful for manipulating products valued in rings / fields.)