Commit 2026-11-10 14:11 37d6c10f
View on Github →chore(Topology/Instances/EReal/Lemmas): golf using positivity and gcongr (#45859) Noticed while taking a look at #45858.
chore(Topology/Instances/EReal/Lemmas): golf using positivity and gcongr (#45859) Noticed while taking a look at #45858.