Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-29 14:39 ce79a27b

View on Github →

feat(analysis/normed_space/pi_Lp): add lemmas about pi_Lp.equiv (#13569) Most of these are trivial dsimp lemmas, but they also let us talk about the norm of constant vectors.

Estimated changes

Modified src/analysis/normed_space/pi_Lp.lean

added theorem pi_Lp.equiv_add

added theorem pi_Lp.equiv_apply

added theorem pi_Lp.equiv_neg

added theorem pi_Lp.equiv_smul

added theorem pi_Lp.equiv_sub

added theorem pi_Lp.equiv_symm_add

added theorem pi_Lp.equiv_symm_apply

added theorem pi_Lp.equiv_symm_neg

added theorem pi_Lp.equiv_symm_smul

added theorem pi_Lp.equiv_symm_sub

added theorem pi_Lp.equiv_symm_zero

added theorem pi_Lp.equiv_zero

added theorem pi_Lp.nnnorm_equiv_symm_const

added theorem pi_Lp.nnnorm_equiv_symm_one

added theorem pi_Lp.norm_equiv_symm_const

added theorem pi_Lp.norm_equiv_symm_one

added theorem pi_Lp.zero_apply