Commit 2026-11-10 23:17 3ab576ff
View on Github →feat({Topology,MeasureTheory}): instances for Additive/Multiplicative (#45174)
This will help me deduce results about automatic continuity of AddChars from the analogous ones for AddMonoidHom.
From MeanFourier
Generated by Claude Sonnet, reviewed line-by-line by myself.
Assisted-by: Claude Sonnet 5.5