Commit 2025-05-11 00:56 2e77c8da

View on Github →

chore(LinearAlgebra/Dual): generalize to semirings (#23933)

Estimated changes

Modified Archive/Sensitivity.lean

Modified Mathlib/Data/Finsupp/Basic.lean

added theorem Finsupp.comapDomain_mapDomain

Modified Mathlib/LinearAlgebra/Dual/Basis.lean

added theorem Basis.eval_injective

modified theorem Basis.eval_ker

modified theorem Basis.linearCombination_coord

modified theorem Basis.sum_dual_apply_smul_coord

modified theorem Module.DualBases.coe_dualBasis

modified theorem Module.DualBases.lc_coeffs

Modified Mathlib/LinearAlgebra/Dual/Defs.lean

Modified Mathlib/LinearAlgebra/Dual/Lemmas.lean

modified theorem Basis.dual_rank_eq

modified theorem Basis.linearEquiv_dual_iff_finiteDimensional

modified theorem Module.comap_eval_surjective

modified theorem Module.eval_apply_eq_zero_iff

modified theorem Module.eval_ker

modified theorem Module.map_eval_injective

modified theorem Module.nontrivial_dual_iff

modified theorem Module.subsingleton_dual_iff

Modified Mathlib/LinearAlgebra/Finsupp/Defs.lean

added theorem Finsupp.leftInverse_lcomapDomain_mapDomain

Modified Mathlib/LinearAlgebra/InvariantBasisNumber.lean

added theorem Module.Finite.exists_nat_not_surjective