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.

Estimated changes