Commit 2025-07-05 07:00 850f9cbd

View on Github →

chore(Algebra/Equiv/TransferInstance): split off group results (#26769) Move group results from Algebra.Equiv.TransferInstance to a new file Algebra.Group.TransferInstance. Additivise a few declarations along the way. This is the first part of #26732, split off for Eric's convenience.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Equiv/TransferInstance.lean

deleted theorem Equiv.div_def

deleted theorem Equiv.inv_def

deleted def Equiv.mulEquiv

deleted theorem Equiv.mulEquiv_apply

deleted theorem Equiv.mulEquiv_symm_apply

deleted theorem Equiv.mul_def

deleted theorem Equiv.one_def

deleted theorem Equiv.pow_def

deleted theorem Equiv.smul_def

deleted theorem Finite.exists_type_univ_nonempty_mulEquiv

Modified Mathlib/Algebra/Group/AddChar.lean

Created Mathlib/Algebra/Group/TransferInstance.lean

added theorem Equiv.div_def

added theorem Equiv.inv_def

added def Equiv.mulEquiv

added theorem Equiv.mulEquiv_apply

added theorem Equiv.mulEquiv_symm_apply

added theorem Equiv.mul_def

added theorem Equiv.one_def

added theorem Equiv.pow_def

added theorem Equiv.smul_def

added theorem Finite.exists_type_univ_nonempty_mulEquiv.{u,

Modified Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean

Modified Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean

Modified Mathlib/CategoryTheory/Galois/Basic.lean

Modified Mathlib/CategoryTheory/Galois/GaloisObjects.lean

Modified Mathlib/CategoryTheory/Localization/CalculusOfFractions/Preadditive.lean

Modified Mathlib/CategoryTheory/Preadditive/Opposite.lean

Modified Mathlib/CategoryTheory/Preadditive/Transfer.lean

Modified Mathlib/Data/Finsupp/MonomialOrder/DegLex.lean

Modified Mathlib/Topology/Homotopy/HomotopyGroup.lean