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

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#563 * leanprover-community/mathlib4#608 * leanprover-community/mathlib4#627 * leanprover-community/mathlib4#638 * leanprover-community/mathlib4#641 * leanprover-community/mathlib4#645 * leanprover-community/mathlib4#650
leanprover-community · Nov 21, 2022 · 4887d72 · 4887d72
1 parent ac3ae21
commit 4887d72
Show file tree

Hide file tree

Showing 9 changed files with 36 additions and 0 deletions.
diff --git a/src/algebra/char_zero/defs.lean b/src/algebra/char_zero/defs.lean
@@ -8,6 +8,10 @@ import data.int.cast.defs
 /-!
 # Characteristic zero
 
+> 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.
+
 A ring `R` is called of characteristic zero if every natural number `n` is non-zero when considered
 as an element of `R`. Since this definition doesn't mention the multiplicative structure of `R`
 except for the existence of `1` in this file characteristic zero is defined for additive monoids

diff --git a/src/algebra/group_with_zero/defs.lean b/src/algebra/group_with_zero/defs.lean
@@ -10,6 +10,10 @@ import algebra.ne_zero
 /-!
 # Typeclasses for groups with an adjoined zero element
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/563
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file provides just the typeclass definitions, and the projection lemmas that expose their
 members.
 

diff --git a/src/algebra/order/hom/basic.lean b/src/algebra/order/hom/basic.lean
@@ -8,6 +8,10 @@ import tactic.positivity
 /-!
 # Algebraic order homomorphism classes
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/627
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines hom classes for common properties at the intersection of order theory and algebra.
 
 ## Typeclasses

diff --git a/src/algebra/order/monoid/lemmas.lean b/src/algebra/order/monoid/lemmas.lean
@@ -9,6 +9,10 @@ import algebra.covariant_and_contravariant
 /-!
 # Ordered monoids
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/608
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file develops the basics of ordered monoids.
 
 ## Implementation details

diff --git a/src/control/ulift.lean b/src/control/ulift.lean
@@ -7,6 +7,10 @@ Authors: Scott Morrison, Jannis Limperg
 /-!
 # Monadic instances for `ulift` and `plift`
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/638
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we define `monad` and `is_lawful_monad` instances on `plift` and `ulift`. -/
 
 universes u v

diff --git a/src/data/int/cast/defs.lean b/src/data/int/cast/defs.lean
@@ -8,6 +8,10 @@ import data.nat.cast.defs
 /-!
 # Cast of integers
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/641
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines the *canonical* homomorphism from the integers into an
 additive group with a one (typically a `ring`).  In additive groups with a one
 element, there exists a unique such homomorphism and we store it in the

diff --git a/src/data/nat/cast/defs.lean b/src/data/nat/cast/defs.lean
@@ -9,6 +9,10 @@ import algebra.ne_zero
 /-!
 # Cast of natural numbers
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/641
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines the *canonical* homomorphism from the natural numbers into an
 `add_monoid` with a one.  In additive monoids with one, there exists a unique
 such homomorphism and we store it in the `nat_cast : ℕ → R` field.

diff --git a/src/data/opposite.lean b/src/data/opposite.lean
@@ -8,6 +8,10 @@ import logic.equiv.defs
 /-!
 # Opposites
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/650
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we define a type synonym `opposite α := α`, denoted by `αᵒᵖ` and two synonyms for the
 identity map, `op : α → αᵒᵖ` and `unop : αᵒᵖ → α`. If `α` is a category, then `αᵒᵖ` is the opposite
 category, with all arrows reversed.

diff --git a/src/order/game_add.lean b/src/order/game_add.lean
@@ -9,6 +9,10 @@ import logic.relation
 /-!
 # Game addition relation
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/645
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines, given relations `rα : α → α → Prop` and `rβ : β → β → Prop`, a relation
 `prod.game_add` on pairs, such that `game_add rα rβ x y` iff `x` can be reached from `y` by
 decreasing either entry (with respect to `rα` and `rβ`). It is so called since it models the