Theorem LinearMap.exists_finsupp_nat_of_fin_fun_injective

Modification history

2025-12-19 08:36
Mathlib/LinearAlgebra/Finsupp/Pi.lean
feat(LinearAlgebra): more on StrongRankCondition (#32194) …
Added LinearMap.exists_finsupp_nat_of_fin_fun_injectiveView on Github →