chore(*): add mathlibport comments

src/algebra/group/order_synonym.lean

@@ -10,6 +10,10 @@ import order.synonym
 /-!
 # Group structure on the order type synonyms
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/651
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Transfer algebraic instances from `α` to `αᵒᵈ` and `lex α`.
 -/
 

src/algebra/hierarchy_design.lean

@@ -8,6 +8,10 @@ import tactic.doc_commands
 /-!
 # Documentation of the algebraic hierarchy
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/656
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A library note giving advice on modifying the algebraic hierarchy.
 (It is not intended as a "tour".)
 

src/algebra/quotient.lean

@@ -8,6 +8,10 @@ import tactic.basic
 /-!
 # Algebraic quotients
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/None
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines notation for algebraic quotients, e.g. quotient groups `G ⧸ H`,
 quotient modules `M ⧸ N` and ideal quotients `R ⧸ I`.
 

src/algebra/ring/defs.lean

@@ -10,6 +10,10 @@ import data.int.cast.defs
 /-!
 # Semirings and rings
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/655
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines semirings, rings and domains. This is analogous to `algebra.group.defs` and
 `algebra.group.basic`, the difference being that the former is about `+` and `*` separately, while
 the present file is about their interaction.