Commit 2024-03-21 18:11 0f2c3bc0

View on Github →

chore(LpSpace): cleanup Fintype/Finite (#11428) Also rename *lpBcf to *lpBCF and drop 2 duplicate instances.

Estimated changes

modified theorem EuclideanSpace.norm_single
modified def EuclideanSpace.single
modified theorem EuclideanSpace.single_apply
modified def EuclideanSpace
modified theorem WithLp.equiv_single
modified theorem WithLp.equiv_symm_single
modified theorem Memℓp.all
added theorem coe_addEquiv_lpBCF
deleted theorem coe_addEquiv_lpBcf
deleted theorem coe_addEquiv_lpBcf_symm
added theorem coe_algEquiv_lpBCF
deleted theorem coe_algEquiv_lpBcf
deleted theorem coe_algEquiv_lpBcf_symm
added theorem coe_lpBCFₗᵢ
added theorem coe_lpBCFₗᵢ_symm
deleted theorem coe_lpBcfₗᵢ
deleted theorem coe_lpBcfₗᵢ_symm
added theorem coe_ringEquiv_lpBCF
deleted theorem coe_ringEquiv_lpBcf
deleted theorem coe_ringEquiv_lpBcf_symm
modified theorem equiv_lpPiLp_norm