leanprover-community · github-actions · Dec 1, 2022
diff --git a/src/algebra/field/defs.lean b/src/algebra/field/defs.lean
@@ -9,6 +9,10 @@ import algebra.ring.defs
 /-!
 # Division (semi)rings and (semi)fields
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/668
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file introduces fields and division rings (also known as skewfields) and proves some basic
 statements about them. For a more extensive theory of fields, see the `field_theory` folder.
 

diff --git a/src/algebra/group/commute.lean b/src/algebra/group/commute.lean
@@ -8,6 +8,10 @@ import algebra.group.semiconj
 /-!
 # Commuting pairs of elements in monoids
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/750
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We define the predicate `commute a b := a * b = b * a` and provide some operations on terms `(h :
 commute a b)`. E.g., if `a`, `b`, and c are elements of a semiring, and that `hb : commute a b` and
 `hc : commute a c`.  Then `hb.pow_left 5` proves `commute (a ^ 5) b` and `(hb.pow_right 2).add_right

diff --git a/src/algebra/group_with_zero/commute.lean b/src/algebra/group_with_zero/commute.lean
@@ -10,6 +10,10 @@ import tactic.nontriviality
 /-!
 # Lemmas about commuting elements in a `monoid_with_zero` or a `group_with_zero`.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/762
+> Any changes to this file require a corresponding PR to mathlib4.
+
 -/
 
 variables {α M₀ G₀ M₀' G₀' F F' : Type*}

diff --git a/src/algebra/group_with_zero/semiconj.lean b/src/algebra/group_with_zero/semiconj.lean
@@ -9,6 +9,10 @@ import algebra.group.semiconj
 /-!
 # Lemmas about semiconjugate elements in a `group_with_zero`.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/757
+> Any changes to this file require a corresponding PR to mathlib4.
+
 -/
 
 variables {α M₀ G₀ M₀' G₀' F F' : Type*}

diff --git a/src/algebra/group_with_zero/units/basic.lean b/src/algebra/group_with_zero/units/basic.lean
@@ -11,6 +11,10 @@ import tactic.assert_exists
 /-!
 # Lemmas about units in a `monoid_with_zero` or a `group_with_zero`.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/735
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We also define `ring.inverse`, a globally defined function on any ring
 (in fact any `monoid_with_zero`), which inverts units and sends non-units to zero.
 -/

diff --git a/src/algebra/hom/embedding.lean b/src/algebra/hom/embedding.lean
@@ -8,6 +8,10 @@ import logic.embedding.basic
 
 /-!
 # The embedding of a cancellative semigroup into itself by multiplication by a fixed element.
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/764
+> Any changes to this file require a corresponding PR to mathlib4.
 -/
 
 variables {R : Type*}

diff --git a/src/algebra/order/monoid/cancel/defs.lean b/src/algebra/order/monoid/cancel/defs.lean
@@ -7,6 +7,10 @@ import algebra.order.monoid.defs
 
 /-!
 # Ordered cancellative monoids
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/774
+> Any changes to this file require a corresponding PR to mathlib4.
 -/
 
 universe u

diff --git a/src/algebra/order/monoid/canonical/defs.lean b/src/algebra/order/monoid/canonical/defs.lean
@@ -10,6 +10,10 @@ import algebra.order.monoid.defs
 
 /-!
 # Canonically ordered monoids
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/778
+> Any changes to this file require a corresponding PR to mathlib4.
 -/
 
 universe u

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

diff --git a/src/algebra/order/monoid/min_max.lean b/src/algebra/order/monoid/min_max.lean
@@ -8,6 +8,10 @@ import algebra.order.monoid.lemmas
 
 /-!
 # Lemmas about `min` and `max` in an ordered monoid.
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/763
+> Any changes to this file require a corresponding PR to mathlib4.
 -/
 
 variables {α β : Type*}

diff --git a/src/algebra/order/monoid/order_dual.lean b/src/algebra/order/monoid/order_dual.lean
@@ -7,7 +7,11 @@ Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Johannes Hölzl
 import algebra.group.order_synonym
 import algebra.order.monoid.cancel.defs
 
-/-! # Ordered monoid structures on the order dual. -/
+/-! # Ordered monoid structures on the order dual. 
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/786
+> Any changes to this file require a corresponding PR to mathlib4.-/
 
 universes u
 variables {α : Type u}

diff --git a/src/algebra/order/sub/defs.lean b/src/algebra/order/sub/defs.lean
@@ -11,6 +11,10 @@ import order.lattice
 /-!
 # Ordered Subtraction
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/732
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file proves lemmas relating (truncated) subtraction with an order. We provide a class
 `has_ordered_sub` stating that `a - b ≤ c ↔ a ≤ c + b`.
 

diff --git a/src/algebra/regular/basic.lean b/src/algebra/regular/basic.lean
@@ -10,6 +10,10 @@ import algebra.group_with_zero.basic
 /-!
 # Regular elements
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/758
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We introduce left-regular, right-regular and regular elements, along with their `to_additive`
 analogues add-left-regular, add-right-regular and add-regular elements.
 

diff --git a/src/algebra/ring/commute.lean b/src/algebra/ring/commute.lean
@@ -10,6 +10,10 @@ import algebra.group.commute
 /-!
 # Semirings and rings
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/759
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file gives lemmas about semirings, rings and domains.
 This is analogous to `algebra.group.basic`,
 the difference being that the former is about `+` and `*` separately, while

diff --git a/src/algebra/ring/regular.lean b/src/algebra/ring/regular.lean
@@ -8,6 +8,10 @@ import algebra.ring.defs
 
 /-!
 # Lemmas about regular elements in rings.
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/795
+> Any changes to this file require a corresponding PR to mathlib4.
 -/
 
 variables {α : Type*}

diff --git a/src/algebra/ring/semiconj.lean b/src/algebra/ring/semiconj.lean
@@ -9,6 +9,10 @@ import algebra.ring.defs
 /-!
 # Semirings and rings
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/751
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file gives lemmas about semirings, rings and domains.
 This is analogous to `algebra.group.basic`,
 the difference being that the former is about `+` and `*` separately, while

diff --git a/src/control/applicative.lean b/src/control/applicative.lean
@@ -9,6 +9,10 @@ import control.functor
 /-!
 # `applicative` instances
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/798
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file provides `applicative` instances for concrete functors:
 * `id`
 * `functor.comp`

diff --git a/src/control/functor.lean b/src/control/functor.lean
@@ -9,6 +9,10 @@ import control.basic
 /-!
 # Functors
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/612
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This module provides additional lemmas, definitions, and instances for `functor`s.
 
 ## Main definitions

diff --git a/src/control/monad/basic.lean b/src/control/monad/basic.lean
@@ -9,6 +9,10 @@ import tactic.basic
 /-!
 # Monad
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/752
+> Any changes to this file require a corresponding PR to mathlib4.
+
 ## Attributes
 
  * ext

diff --git a/src/data/countable/defs.lean b/src/data/countable/defs.lean
@@ -8,6 +8,10 @@ import data.finite.defs
 /-!
 # Countable types
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/736
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we define a typeclass saying that a given `Sort*` is countable. See also `encodable`
 for a version that singles out a specific encoding of elements of `α` by natural numbers.
 

diff --git a/src/data/int/units.lean b/src/data/int/units.lean
@@ -10,6 +10,10 @@ import algebra.ring.units
 
 /-!
 # Lemmas about units in `ℤ`.
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/807
+> Any changes to this file require a corresponding PR to mathlib4.
 -/
 
 namespace int

diff --git a/src/data/nat/basic.lean b/src/data/nat/basic.lean
@@ -10,6 +10,10 @@ import algebra.ring.defs
 /-!
 # Basic operations on the natural numbers
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/729
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file contains:
 - instances on the natural numbers
 - some basic lemmas about natural numbers

diff --git a/src/data/nat/psub.lean b/src/data/nat/psub.lean
@@ -8,6 +8,10 @@ import data.nat.basic
 /-!
 # Partial predecessor and partial subtraction on the natural numbers
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/806
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The usual definition of natural number subtraction (`nat.sub`) returns 0 as a "garbage value" for
 `a - b` when `a < b`. Similarly, `nat.pred 0` is defined to be `0`. The functions in this file
 wrap the result in an `option` type instead:

diff --git a/src/data/nat/units.lean b/src/data/nat/units.lean
@@ -6,7 +6,11 @@ Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad, Mario Carneiro
 import data.nat.basic
 import algebra.group.units
 
-/-! # The units of the natural numbers as a `monoid` and `add_monoid` -/
+/-! # The units of the natural numbers as a `monoid` and `add_monoid` 
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/805
+> Any changes to this file require a corresponding PR to mathlib4.-/
 
 namespace nat
 

diff --git a/src/data/pi/algebra.lean b/src/data/pi/algebra.lean
@@ -15,6 +15,10 @@ import data.prod.basic
 /-!
 # Instances and theorems on pi types
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/564
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file provides basic definitions and notation instances for Pi types.
 
 Instances of more sophisticated classes are defined in `pi.lean` files elsewhere.

diff --git a/src/data/prod/lex.lean b/src/data/prod/lex.lean
@@ -8,6 +8,10 @@ import order.bounded_order
 /-!
 # Lexicographic order
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/783
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines the lexicographic relation for pairs of orders, partial orders and linear orders.
 
 ## Main declarations

diff --git a/src/logic/embedding/basic.lean b/src/logic/embedding/basic.lean
@@ -12,6 +12,10 @@ import logic.equiv.basic
 
 /-!
 # Injective functions
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/700
+> Any changes to this file require a corresponding PR to mathlib4.
 -/
 
 universes u v w x

diff --git a/src/logic/equiv/option.lean b/src/logic/equiv/option.lean
@@ -11,6 +11,10 @@ import logic.equiv.defs
 /-!
 # Equivalences for `option α`
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/674
+> Any changes to this file require a corresponding PR to mathlib4.
+
 
 We define
 * `equiv.option_congr`: the `option α ≃ option β` constructed from `e : α ≃ β` by sending `none` to

diff --git a/src/order/bounded_order.lean b/src/order/bounded_order.lean
@@ -9,6 +9,10 @@ import data.option.basic
 /-!
 # ⊤ and ⊥, bounded lattices and variants
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/697
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines top and bottom elements (greatest and least elements) of a type, the bounded
 variants of different kinds of lattices, sets up the typeclass hierarchy between them and provides
 instances for `Prop` and `fun`.

diff --git a/src/order/disjoint.lean b/src/order/disjoint.lean
@@ -8,6 +8,10 @@ import order.bounded_order
 /-!
 # Disjointness and complements
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/773
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines `disjoint`, `codisjoint`, and the `is_compl` predicate.
 
 ## Main declarations

diff --git a/src/order/min_max.lean b/src/order/min_max.lean
@@ -8,6 +8,10 @@ import order.lattice
 /-!
 # `max` and `min`
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/728
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file proves basic properties about maxima and minima on a `linear_order`.
 
 ## Tags

diff --git a/src/order/prop_instances.lean b/src/order/prop_instances.lean
@@ -10,6 +10,10 @@ import order.with_bot
 
 # The order on `Prop`
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/792
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Instances on `Prop` such as `distrib_lattice`, `bounded_order`, `linear_order`.
 
 -/

diff --git a/src/order/rel_iso/basic.lean b/src/order/rel_iso/basic.lean
@@ -10,6 +10,10 @@ import order.rel_classes
 /-!
 # Relation homomorphisms, embeddings, isomorphisms
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/772
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines relation homomorphisms, embeddings, isomorphisms and order embeddings and
 isomorphisms.
 

diff --git a/src/order/with_bot.lean b/src/order/with_bot.lean
@@ -8,6 +8,10 @@ import order.bounded_order
 /-!
 # `with_bot`, `with_top`
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/776
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Adding a `bot` or a `top` to an order.
 
 ## Main declarations