Commit 2024-12-03 15:10 c5be7923
View on Github →refactor(Quot): use dependent arrows in congruence arguments for map
and map₂
(#15127)
The map
and map₂
functions for Quot
and Quotient
used a Lean 3 version of congruence arguments that avoids dependent arrows. This PR changes those arguments to have the more recognizable formulation of congruence.