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.

Estimated changes