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

Modified Mathlib/Algebra/GCDMonoid/Basic.lean

Modified Mathlib/Data/Quot.lean

modified theorem Quotient.map_mk

deleted theorem Quotient.map₂'_mk''

modified theorem Quotient.map₂_mk

Modified Mathlib/Data/Setoid/Basic.lean

Modified Mathlib/GroupTheory/Congruence/Defs.lean

Modified Mathlib/LinearAlgebra/Projectivization/Constructions.lean

Modified Mathlib/Order/Filter/Germ/Basic.lean

Modified Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean

Modified Mathlib/Topology/Algebra/SeparationQuotient/Basic.lean