Commit 2023-08-30 22:54 bfb6bb73

View on Github →

refactor: remove PiLp.equiv (#6501) This removes the (PiLp.equiv 2 fun i => α i) abbreviation, replacing it with its implementation (WithLp.equiv 2 (∀ i, α i)). The same thing is done for PiLp.linearEquiv.

Estimated changes

deleted theorem PiLp.equiv_single
deleted theorem PiLp.equiv_symm_single
added theorem WithLp.equiv_single
modified theorem Matrix.frobenius_nnnorm_col
modified theorem Matrix.frobenius_nnnorm_row
modified theorem Matrix.frobenius_norm_col
modified theorem Matrix.frobenius_norm_row
modified theorem PiLp.basisFun_equivFun
modified theorem PiLp.continuous_equiv
modified theorem PiLp.continuous_equiv_symm
deleted theorem PiLp.equiv_apply
deleted theorem PiLp.equiv_symm_apply
modified theorem PiLp.infty_equiv_isometry
modified theorem PiLp.lipschitzWith_equiv
modified theorem PiLp.norm_equiv_symm_single
added theorem WithLp.equiv_pi_apply