Commit 2026-07-16 14:39 f2e1a516

View on Github →

feat(LinearAlgebra/Contraction): bijectivity of dualTensorHom + generalize to CommSemiring (#40297) migrated from #25284

Estimated changes

Modified Mathlib/Data/Finsupp/Defs.lean

added theorem Finsupp.mapRange_bijective

Modified Mathlib/LinearAlgebra/Contraction.lean

added theorem Module.Finite.of_one_mem_range_dualTensorHom

added theorem Module.Projective.of_one_mem_range_dualTensorHom

added theorem coe_dualTensorHomEquivOfBasis

added theorem dualTensorHomEquiv_eq_dualTensorHomEquivOfBasis

added theorem dualTensorHom_bijective

added theorem dualTensorHom_bijective_of_comp_eq_id_right

added theorem dualTensorHom_bijective_of_finite_left_projective_right

added theorem dualTensorHom_bijective_of_finite_projective_right

added theorem dualTensorHom_comp_lTensor

added theorem dualTensorHom_comp_rTensor_dualMap

added theorem dualTensorHom_finsupp

added theorem dualTensorHom_finsupp_bijective

added theorem dualTensorHom_fun_bijective

added theorem dualTensorHom_self_right

Modified Mathlib/LinearAlgebra/Pi.lean

added def LinearEquiv.linearMapPi

Modified Mathlib/LinearAlgebra/Trace.lean

Modified Mathlib/RingTheory/Finiteness/Finsupp.lean

added theorem LinearMap.finsuppLinearMap_bijective_of_finite

added theorem LinearMap.finsuppLinearMap_bijective_of_moduleFinite

added theorem LinearMap.finsuppLinearMap_injective