Mathlib v3 is deprecated. Go to Mathlib v4

Theorem basis.equiv_fun_of_equiv_fun

Modification history

2023-05-22 08:06

src/linear_algebra/basis.lean

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

Added basis.equiv_fun_of_equiv_fun View on Github →