Commit 2024-12-20 13:13 49f1292b

View on Github →

chore: move Logic.Equiv.TransferInstance to Algebra.Equiv.TransferInstance (#19993)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Category/ModuleCat/EnoughInjectives.lean

Renamed Mathlib/Logic/Equiv/TransferInstance.lean to Mathlib/Algebra/Equiv/TransferInstance.lean

Modified Mathlib/Algebra/Group/AddChar.lean

Modified Mathlib/Algebra/Module/Injective.lean

Modified Mathlib/CategoryTheory/Abelian/Transfer.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/Data/Finsupp/MonomialOrder/DegLex.lean

Modified Mathlib/Logic/Equiv/Basic.lean

Modified Mathlib/Logic/Equiv/Defs.lean

Modified Mathlib/Logic/Small/Group.lean

Modified Mathlib/Logic/Small/Ring.lean

Modified Mathlib/RingTheory/LocalRing/RingHom/Basic.lean

Modified Mathlib/RingTheory/OrzechProperty.lean

Modified Mathlib/RingTheory/Regular/RegularSequence.lean

Modified Mathlib/Topology/Algebra/UniformRing.lean

Modified Mathlib/Topology/Homotopy/HomotopyGroup.lean