Commit 2023-05-22 08:06 13bce9a6

View on Github →

chore(linear_algebra/basis): simp lemmas about basis.equiv_fun (#19021)

Estimated changes

Modified src/analysis/inner_product_space/pi_L2.lean

Modified src/analysis/normed_space/pi_Lp.lean

added theorem pi_Lp.basis_fun_equiv_fun

Modified src/linear_algebra/basis.lean

added theorem basis.equiv_fun_of_equiv_fun

Modified src/linear_algebra/std_basis.lean

added theorem pi.basis_fun_equiv_fun