Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Theorem
basis.to_dual_equiv_apply
Modification history
2023-05-07 21:39
src/linear_algebra/dual.lean
refactor(linear_algebra/dual): make `module.dual` reducible (#18963) …
Added
basis.to_dual_equiv_apply
View on Github →