Commit 2024-07-05 09:16 56d9d0ab
View on Github →chore(Mathlib/Data/Equiv/Functor): deduplicate Functor.mapEquiv
(#14381)
Functor.map_equiv
in Mathlib.Data.Equiv.Functor
is a duplication of Functor.mapEquiv
in Mathlib.Logic.Equiv.Functor
so should be removed.