Theorem LinearMap.finsuppLinearMap_bijective_of_moduleFinite

Modification history

2026-07-16 14:39
Mathlib/RingTheory/Finiteness/Finsupp.lean
feat(LinearAlgebra/Contraction): bijectivity of `dualTensorHom` + generalize to `CommSemiring` (#40297) …
Added LinearMap.finsuppLinearMap_bijective_of_moduleFiniteView on Github →