Commit 2025-06-23 08:19 b38e0af9
View on Github →chore: fix WithLp defeq abuse (#26248)
The lemma WithLp.prod_inner_apply contained x.1 with x : WithLp 2 (E × F). Replace it with (WithLp.equiv 2 (E × F) x).fst.
chore: fix WithLp defeq abuse (#26248)
The lemma WithLp.prod_inner_apply contained x.1 with x : WithLp 2 (E × F). Replace it with (WithLp.equiv 2 (E × F) x).fst.