Commit 2024-02-23 00:32 9e2d5175

View on Github →

fix(Analysis/Normed/Group): make instance helpers reducible (#10726) Zulip thread This slightly simplifies two downstream proofs, as a bonus.

Estimated changes

modified def NormedGroup.induced