Commit 2022-09-25 21:25 74f6e95c
View on Github →feat(data/real/ennreal): make of_real_sub easier to rewrite with (#16621)
A tiny edit to make this lemma more general for the purpose of rewriting - previously q was only for nnreal (even though it had the assumption of nonnegativity).