Mathlib v3 is deprecated. Go to Mathlib v4

Theorem pi_Lp.basis_fun_equiv_fun

Modification history

2023-05-22 08:06
src/analysis/normed_space/pi_Lp.lean
chore(linear_algebra/basis): `simp` lemmas about `basis.equiv_fun` (#19021)
Added pi_Lp.basis_fun_equiv_funView on Github →