Commit 2024-06-21 21:56 23725d3c

View on Github →

chore: deprecate AlgEquiv.map_* lemmas (#14005) These are redundant.

Estimated changes

Modified Mathlib/Algebra/Algebra/Equiv.lean

deleted theorem AlgEquiv.map_finsupp_prod

deleted theorem AlgEquiv.map_finsupp_sum

deleted theorem AlgEquiv.map_prod

deleted theorem AlgEquiv.map_smul

Modified Mathlib/Algebra/Algebra/Operations.lean

Modified Mathlib/Algebra/MvPolynomial/Equiv.lean

Modified Mathlib/Algebra/MvPolynomial/Funext.lean

Modified Mathlib/FieldTheory/AbelRuffini.lean

Modified Mathlib/FieldTheory/Adjoin.lean

Modified Mathlib/FieldTheory/KummerExtension.lean

Modified Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean

Modified Mathlib/LinearAlgebra/Matrix/Charpoly/Basic.lean

Modified Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean

Modified Mathlib/LinearAlgebra/Matrix/Charpoly/FiniteField.lean

Modified Mathlib/LinearAlgebra/Matrix/Reindex.lean

Modified Mathlib/NumberTheory/FunctionField.lean

Modified Mathlib/RingTheory/Localization/Basic.lean

Modified Mathlib/RingTheory/PowerBasis.lean

Modified Mathlib/RingTheory/RootsOfUnity/Basic.lean