chore(algebra/*): mark frozen files that have been ported to mathlib4 (…

…#17039)

This is chiefly a proposal that we get started marking files as frozen, and a proposal for a specific format.

Once we settle on what gets written here, we should add some CI that adds a special label to any PR modifying a frozen file.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/algebra/abs.lean

@@ -7,6 +7,10 @@ Authors: Christopher Hoskin
 /-!
 # Absolute value
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/477
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines a notational class `has_abs` which adds the unary operator `abs` and the notation
 `|.|`. The concept of an absolute value occurs in lattice ordered groups and in GL and GM spaces.
 

src/algebra/covariant_and_contravariant.lean

@@ -12,6 +12,10 @@ import order.monotone
 
 # Covariants and contravariants
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/467
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file contains general lemmas and instances to work with the interactions between a relation and
 an action on a Type.
 

src/algebra/group/basic.lean

@@ -9,6 +9,10 @@ import algebra.group.defs
 /-!
 # Basic lemmas about semigroups, monoids, and groups
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/457
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file lists various basic lemmas about semigroups, monoids, and groups. Most proofs are
 one-liners from the corresponding axioms. For the definitions of semigroups, monoids and groups, see
 `algebra/group/defs.lean`.

src/algebra/group/defs.lean

@@ -9,6 +9,10 @@ import tactic.basic
 /-!
 # Typeclasses for (semi)groups and monoids
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/457
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we define typeclasses for algebraic structures with one binary operation.
 The classes are named `(add_)?(comm_)?(semigroup|monoid|group)`, where `add_` means that
 the class uses additive notation and `comm_` means that the class assumes that the binary

src/logic/relator.lean

@@ -2,12 +2,19 @@
 Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
-
-Relator for functions, pairs, sums, and lists.
 -/
 
 import logic.basic
 
+/-!
+# Relator for functions, pairs, sums, and lists.
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/385
+> Any changes to this file require a corresponding PR to mathlib4.
+
+-/
+
 namespace relator
 universes u₁ u₂ v₁ v₂