Commit 2023-08-14 01:22 484cfebd

View on Github →

refactor: generalize PiLp to WithLp (#6409) The motivation is to be able to reuse this for ProdLp in #6136. This matches the pattern of how the Lex type synonym is used.

Estimated changes

deleted theorem PiLp.equiv_add
deleted theorem PiLp.equiv_neg
deleted theorem PiLp.equiv_smul
deleted theorem PiLp.equiv_sub
deleted theorem PiLp.equiv_symm_add
deleted theorem PiLp.equiv_symm_neg
deleted theorem PiLp.equiv_symm_smul
deleted theorem PiLp.equiv_symm_sub
deleted theorem PiLp.equiv_symm_zero
deleted theorem PiLp.equiv_zero
deleted def PiLp
added theorem WithLp.equiv_add
added theorem WithLp.equiv_neg
added theorem WithLp.equiv_smul
added theorem WithLp.equiv_sub
added theorem WithLp.equiv_symm_add
added theorem WithLp.equiv_symm_neg
added theorem WithLp.equiv_symm_smul
added theorem WithLp.equiv_symm_sub
added theorem WithLp.equiv_symm_zero
added theorem WithLp.equiv_zero
added def WithLp