chore(*): add mathlibport comments (#17686)

Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status). Relates to the following PRs: * leanprover-community/mathlib4#643 * leanprover-community/mathlib4#646 * leanprover-community/mathlib4#648 * leanprover-community/mathlib4#649 * leanprover-community/mathlib4#651 * leanprover-community/mathlib4#655 * leanprover-community/mathlib4#656 * leanprover-community/mathlib4#657 * leanprover-community/mathlib4#661 * leanprover-community/mathlib4#670 * leanprover-community/mathlib4#671 * leanprover-community/mathlib4#672 * leanprover-community/mathlib4#686
leanprover-community · Nov 23, 2022 · 4afb682 · 4afb682
1 parent 6d0c451
commit 4afb682
Show file tree

Hide file tree

Showing 13 changed files with 49 additions and 1 deletion.
diff --git a/src/algebra/char_zero/defs.lean b/src/algebra/char_zero/defs.lean
@@ -9,7 +9,7 @@ import data.int.cast.defs
 # Characteristic zero
 
 > THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
-> https://github.com/leanprover-community/mathlib4/pull/None
+> https://github.com/leanprover-community/mathlib4/pull/661
 > Any changes to this file require a corresponding PR to mathlib4.
 
 A ring `R` is called of characteristic zero if every natural number `n` is non-zero when considered

diff --git a/src/algebra/group/order_synonym.lean b/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 α`.
 -/
 

diff --git a/src/algebra/hierarchy_design.lean b/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/657
+> 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".)
 

diff --git a/src/algebra/quotient.lean b/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/643
+> 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`.
 

diff --git a/src/algebra/ring/defs.lean b/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.

diff --git a/src/algebra/ring/order_synonym.lean b/src/algebra/ring/order_synonym.lean
@@ -9,6 +9,10 @@ import algebra.group.order_synonym
 /-!
 # Ring structure on the order type synonyms
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/671
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Transfer algebraic instances from `α` to `αᵒᵈ` and `lex α`.
 -/
 

diff --git a/src/control/equiv_functor.lean b/src/control/equiv_functor.lean
@@ -8,6 +8,10 @@ import logic.equiv.defs
 /-!
 # Functions functorial with respect to equivalences
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/649
+> Any changes to this file require a corresponding PR to mathlib4.
+
 An `equiv_functor` is a function from `Type → Type` equipped with the additional data of
 coherently mapping equivalences to equivalences.
 

diff --git a/src/data/int/cast/basic.lean b/src/data/int/cast/basic.lean
@@ -9,6 +9,10 @@ import algebra.group.basic
 /-!
 # Cast of integers (additional theorems)
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/670
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file proves additional properties about the *canonical* homomorphism from
 the integers into an additive group with a one (`int.cast`).
 

diff --git a/src/data/lazy_list.lean b/src/data/lazy_list.lean
@@ -7,6 +7,10 @@ Authors: Leonardo de Moura
 /-!
 # Lazy lists
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/686
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The type `lazy_list α` is a lazy list with elements of type `α`.
 In the VM, these are potentially infinite lists
 where all elements after the first are computed on-demand.

diff --git a/src/data/list/lex.lean b/src/data/list/lex.lean
@@ -8,6 +8,10 @@ import order.rel_classes
 /-!
 # Lexicographic ordering of lists.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/672
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The lexicographic order on `list α` is defined by `L < M` iff
 * `[] < (a :: L)` for any `a` and `L`,
 * `(a :: L) < (b :: M)` where `a < b`, or

diff --git a/src/data/option/n_ary.lean b/src/data/option/n_ary.lean
@@ -8,6 +8,10 @@ import data.option.basic
 /-!
 # Binary map of options
 
+> 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.
+
 This file defines the binary map of `option`. This is mostly useful to define pointwise operations
 on intervals.
 

diff --git a/src/data/sigma/lex.lean b/src/data/sigma/lex.lean
@@ -9,6 +9,10 @@ import order.rel_classes
 /-!
 # Lexicographic order on a sigma type
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/646
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This defines the lexicographical order of two arbitrary relations on a sigma type and proves some
 lemmas about `psigma.lex`, which is defined in core Lean.
 

diff --git a/src/order/iterate.lean b/src/order/iterate.lean
@@ -9,6 +9,10 @@ import order.monotone
 /-!
 # Inequalities on iterates
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/648
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we prove some inequalities comparing `f^[n] x` and `g^[n] x` where `f` and `g` are
 two self-maps that commute with each other.