chore(data/quot): freeze (#17479)

leanprover-community · Nov 12, 2022 · d337708 · d337708
1 parent f435f95
commit d337708
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/src/data/quot.lean b/src/data/quot.lean
@@ -8,6 +8,10 @@ import logic.relator
 /-!
 # Quotient types
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/559
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This module extends the core library's treatment of quotient types (`init.data.quot`).
 
 ## Tags