diff --git a/src/order/irreducible.lean b/src/order/irreducible.lean
index 07bec21729d7c..0862574732a13 100644
--- a/src/order/irreducible.lean
+++ b/src/order/irreducible.lean
@@ -9,6 +9,9 @@ import data.fintype.card
 /-!
 # Irreducible and prime elements in an order
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines irreducible and prime elements in an order and shows that in a well-founded
 lattice every element decomposes as a supremum of irreducible elements.