Commit 2026-08-14 05:41 4d476f6d

View on Github →

chore(Data/Finsupp): make mapDomain_congr congr (#39575) This makes simp stronger. It particular, it breaks some proofs that relied on simp being weak. From MeanFourier

Estimated changes

Modified Mathlib/Algebra/MonoidAlgebra/MapDomain.lean

Modified Mathlib/Algebra/MonoidAlgebra/Module.lean

Modified Mathlib/Algebra/MvPolynomial/Nilpotent.lean

Modified Mathlib/Algebra/Polynomial/Laurent.lean

Modified Mathlib/Data/Finsupp/Basic.lean

modified theorem Finsupp.mapDomain_congr

added theorem Finsupp.mapDomain_fun_comp

modified theorem Finsupp.mapDomain_id

Modified Mathlib/Geometry/Convex/ConvexSpace/Defs.lean

Modified Mathlib/LinearAlgebra/Basis/Defs.lean

modified theorem Module.Basis.repr_reindex

Modified Mathlib/LinearAlgebra/Finsupp/Pi.lean

Modified Mathlib/LinearAlgebra/Matrix/Basis.lean

Modified Mathlib/NumberTheory/NumberField/EquivReindex.lean

Modified Mathlib/NumberTheory/NumberField/House.lean

Modified Mathlib/RepresentationTheory/Homological/GroupHomology/Functoriality.lean

Modified Mathlib/RepresentationTheory/Intertwining.lean

added theorem Representation.IntertwiningMap.coe_id

modified theorem Representation.IntertwiningMap.id_apply

Modified Mathlib/RingTheory/Bialgebra/MonoidAlgebra.lean