Commit 2023-05-23 22:59 4f3556f8

View on Github →

chore: forward-port leanprover-community/mathlib#19021 (#4257)

Estimated changes

Modified Mathlib/LinearAlgebra/Basis.lean

added theorem Basis.equivFun_ofEquivFun

Modified Mathlib/LinearAlgebra/StdBasis.lean

added theorem Pi.basisFun_equivFun