Commit 2025-04-13 16:12 e8a574a8
View on Github →chore(tprod): move tprod lemmas to protected namespace (#23959)
As per zulip discussion, this PR renames lemmas of the form
theorem tprod_foo {f : a -> b} (Multipliable f) : _
to
protected theorem Multipliable.tprod_foo {f : a -> b} (Multipliable f) : _,
and similar for tsum/Summable, usually via to_additive. This is so the name tprod_foo (and by extension tsum_foo) is freed up for planned versions of the lemmas in settings where multipliabilty/summability automatically holds (such as ENat and ENNReal for summability).
We also deprecate all the old names.