Commit 2025-09-05 08:31 dc2f7b72
View on Github →feat(Mathlib/Data/Quot.lean): revive Quotient.map₂' (#29359)
It looks like it was unintentionally deleted in #15127.
feat(Mathlib/Data/Quot.lean): revive Quotient.map₂' (#29359)
It looks like it was unintentionally deleted in #15127.