Commit 2023-02-08 20:27 38d38e09
View on Github →chore(analysis/normed_space/pi_Lp): pi_Lp.equiv is continuous (#18402) The main benefit here is that this should now work with the continuity tactic.
chore(analysis/normed_space/pi_Lp): pi_Lp.equiv is continuous (#18402) The main benefit here is that this should now work with the continuity tactic.