Mathlib Changelog
v4
Changelog
About
Github
Theorem
Basis.equivFun_ofEquivFun
Modification history
2024-02-04 23:05
Mathlib/LinearAlgebra/Basis.lean
feat(LinearAlgebra/Basis): assume `[Finite ι]` instead of `[Fintype ι]` (#10251)
Modified
Basis.equivFun_ofEquivFun
View on Github →
2023-05-23 22:59
Mathlib/LinearAlgebra/Basis.lean
chore: forward-port leanprover-community/mathlib#19021 (#4257)
Added
Basis.equivFun_ofEquivFun
View on Github →