chore: add source headers to ported theory files (#1094)

The script used to do this is included. The yaml file was obtained from https://raw.githubusercontent.com/wiki/leanprover-community/mathlib/mathlib4-port-status.md
leanprover-community · Dec 18, 2022 · f168625 · f168625
1 parent f0939b2
commit f168625
Show file tree

Hide file tree

Showing 268 changed files with 1,399 additions and 0 deletions.
diff --git a/Mathlib/Algebra/Abs.lean b/Mathlib/Algebra/Abs.lean
@@ -2,6 +2,11 @@
 Copyright (c) 2021 Christopher Hoskin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Christopher Hoskin
+
+! This file was ported from Lean 3 source module algebra.abs
+! leanprover-community/mathlib commit c4658a649d216f57e99621708b09dcb3dcccbd23
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
 -/
 import Mathlib.Mathport.Rename
 /-!

diff --git a/Mathlib/Algebra/CharZero/Defs.lean b/Mathlib/Algebra/CharZero/Defs.lean
@@ -2,6 +2,11 @@
 Copyright (c) 2014 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
+
+! This file was ported from Lean 3 source module algebra.char_zero.defs
+! leanprover-community/mathlib commit d6aae1bcbd04b8de2022b9b83a5b5b10e10c777d
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
 -/
 import Mathlib.Data.Int.Cast.Defs
 import Mathlib.Tactic.NormCast.Tactic

diff --git a/Mathlib/Algebra/CovariantAndContravariant.lean b/Mathlib/Algebra/CovariantAndContravariant.lean
@@ -2,6 +2,11 @@
 Copyright (c) 2021 Damiano Testa. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Damiano Testa
+
+! This file was ported from Lean 3 source module algebra.covariant_and_contravariant
+! leanprover-community/mathlib commit c4658a649d216f57e99621708b09dcb3dcccbd23
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
 -/
 import Mathlib.Algebra.Group.Defs
 import Mathlib.Order.Basic

diff --git a/Mathlib/Algebra/Divisibility/Basic.lean b/Mathlib/Algebra/Divisibility/Basic.lean
@@ -4,6 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Amelia Livingston, Yury Kudryashov,
 Neil Strickland, Aaron Anderson
 Ported by: Matej Penciak
+
+! This file was ported from Lean 3 source module algebra.divisibility.basic
+! leanprover-community/mathlib commit 70d50ecfd4900dd6d328da39ab7ebd516abe4025
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
 -/
 import Mathlib.Algebra.Hom.Group
 

diff --git a/Mathlib/Algebra/Divisibility/Units.lean b/Mathlib/Algebra/Divisibility/Units.lean
@@ -4,6 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Amelia Livingston, Yury Kudryashov,
 Neil Strickland, Aaron Anderson
 Ported by: Joël Riou
+
+! This file was ported from Lean 3 source module algebra.divisibility.units
+! leanprover-community/mathlib commit e574b1a4e891376b0ef974b926da39e05da12a06
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
 -/
 import Mathlib.Algebra.Divisibility.Basic
 import Mathlib.Algebra.Group.Units

diff --git a/Mathlib/Algebra/EuclideanDomain/Basic.lean b/Mathlib/Algebra/EuclideanDomain/Basic.lean
@@ -2,6 +2,11 @@
 Copyright (c) 2018 Louis Carlin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Louis Carlin, Mario Carneiro
+
+! This file was ported from Lean 3 source module algebra.euclidean_domain.basic
+! leanprover-community/mathlib commit 655994e298904d7e5bbd1e18c95defd7b543eb94
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
 -/
 import Mathlib.Algebra.EuclideanDomain.Defs
 import Mathlib.Algebra.Ring.Divisibility

diff --git a/Mathlib/Algebra/EuclideanDomain/Defs.lean b/Mathlib/Algebra/EuclideanDomain/Defs.lean
@@ -2,6 +2,11 @@
 Copyright (c) 2018 Louis Carlin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Louis Carlin, Mario Carneiro
+
+! This file was ported from Lean 3 source module algebra.euclidean_domain.defs
+! leanprover-community/mathlib commit f1a2caaf51ef593799107fe9a8d5e411599f3996
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
 -/
 import Mathlib.Logic.Nontrivial
 import Mathlib.Algebra.Divisibility.Basic

diff --git a/Mathlib/Algebra/Field/Basic.lean b/Mathlib/Algebra/Field/Basic.lean
@@ -2,6 +2,11 @@
 Copyright (c) 2014 Robert Lewis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Lewis, Leonardo de Moura, Johannes Hölzl, Mario Carneiro
+
+! This file was ported from Lean 3 source module algebra.field.basic
+! leanprover-community/mathlib commit fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
 -/
 import Mathlib.Algebra.Field.Defs
 import Mathlib.Algebra.GroupWithZero.Units.Lemmas

diff --git a/Mathlib/Algebra/Field/Defs.lean b/Mathlib/Algebra/Field/Defs.lean
@@ -2,6 +2,11 @@
 Copyright (c) 2014 Robert Lewis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Lewis, Leonardo de Moura, Johannes Hölzl, Mario Carneiro
+
+! This file was ported from Lean 3 source module algebra.field.defs
+! leanprover-community/mathlib commit 70d50ecfd4900dd6d328da39ab7ebd516abe4025
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
 -/
 
 import Mathlib.Algebra.Ring.Defs

diff --git a/Mathlib/Algebra/Group/Basic.lean b/Mathlib/Algebra/Group/Basic.lean
@@ -2,6 +2,11 @@
 Copyright (c) 2014 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Simon Hudon, Mario Carneiro
+
+! This file was ported from Lean 3 source module algebra.group.basic
+! leanprover-community/mathlib commit d6aae1bcbd04b8de2022b9b83a5b5b10e10c777d
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
 -/
 import Mathlib.Algebra.Group.Defs
 

diff --git a/Mathlib/Algebra/Group/Commutator.lean b/Mathlib/Algebra/Group/Commutator.lean
@@ -2,6 +2,11 @@
 Copyright (c) 2022 Thomas Browning. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Thomas Browning
+
+! This file was ported from Lean 3 source module algebra.group.commutator
+! leanprover-community/mathlib commit c4658a649d216f57e99621708b09dcb3dcccbd23
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
 -/
 import Mathlib.Algebra.Group.Defs
 import Mathlib.Data.Bracket

diff --git a/Mathlib/Algebra/Group/Commute.lean b/Mathlib/Algebra/Group/Commute.lean
@@ -2,6 +2,11 @@
 Copyright (c) 2019 Neil Strickland. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Neil Strickland, Yury Kudryashov
+
+! This file was ported from Lean 3 source module algebra.group.commute
+! leanprover-community/mathlib commit 70d50ecfd4900dd6d328da39ab7ebd516abe4025
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
 -/
 import Mathlib.Algebra.Group.Semiconj
 

diff --git a/Mathlib/Algebra/Group/Defs.lean b/Mathlib/Algebra/Group/Defs.lean
@@ -2,6 +2,11 @@
 Copyright (c) 2014 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Simon Hudon, Mario Carneiro
+
+! This file was ported from Lean 3 source module algebra.group.defs
+! leanprover-community/mathlib commit 41cf0cc2f528dd40a8f2db167ea4fb37b8fde7f3
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
 -/
 
 import Mathlib.Init.ZeroOne

diff --git a/Mathlib/Algebra/Group/Ext.lean b/Mathlib/Algebra/Group/Ext.lean
@@ -2,6 +2,11 @@
 Copyright (c) 2021 Bryan Gin-ge Chen. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bryan Gin-ge Chen, Yury Kudryashov
+
+! This file was ported from Lean 3 source module algebra.group.ext
+! leanprover-community/mathlib commit e574b1a4e891376b0ef974b926da39e05da12a06
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
 -/
 import Mathlib.Algebra.Hom.Group
 import Mathlib.Tactic.Basic

diff --git a/Mathlib/Algebra/Group/InjSurj.lean b/Mathlib/Algebra/Group/InjSurj.lean
@@ -2,6 +2,11 @@
 Copyright (c) 2020 Johan Commelin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
+
+! This file was ported from Lean 3 source module algebra.group.inj_surj
+! leanprover-community/mathlib commit d6aae1bcbd04b8de2022b9b83a5b5b10e10c777d
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
 -/
 import Mathlib.Algebra.Group.Defs
 import Mathlib.Logic.Function.Basic

diff --git a/Mathlib/Algebra/Group/Opposite.lean b/Mathlib/Algebra/Group/Opposite.lean
@@ -2,6 +2,11 @@
 Copyright (c) 2018 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau
+
+! This file was ported from Lean 3 source module algebra.group.opposite
+! leanprover-community/mathlib commit 655994e298904d7e5bbd1e18c95defd7b543eb94
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
 -/
 import Mathlib.Algebra.Group.InjSurj
 import Mathlib.Algebra.Group.Commute

diff --git a/Mathlib/Algebra/Group/OrderSynonym.lean b/Mathlib/Algebra/Group/OrderSynonym.lean
@@ -2,6 +2,11 @@
 Copyright (c) 2021 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov, Yaël Dillies
+
+! This file was ported from Lean 3 source module algebra.group.order_synonym
+! leanprover-community/mathlib commit d6aae1bcbd04b8de2022b9b83a5b5b10e10c777d
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
 -/
 import Mathlib.Algebra.Group.Defs
 import Mathlib.Order.Synonym

diff --git a/Mathlib/Algebra/Group/Prod.lean b/Mathlib/Algebra/Group/Prod.lean
@@ -2,6 +2,11 @@
 Copyright (c) 2020 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon, Patrick Massot, Yury Kudryashov
+
+! This file was ported from Lean 3 source module algebra.group.prod
+! leanprover-community/mathlib commit cf9386b56953fb40904843af98b7a80757bbe7f9
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
 -/
 import Mathlib.Algebra.Group.Opposite
 import Mathlib.Algebra.GroupWithZero.Units.Basic

diff --git a/Mathlib/Algebra/Group/Semiconj.lean b/Mathlib/Algebra/Group/Semiconj.lean
@@ -4,6 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 
 Some proofs and docs came from `algebra/commute` (c) Neil Strickland
+
+! This file was ported from Lean 3 source module algebra.group.semiconj
+! leanprover-community/mathlib commit a148d797a1094ab554ad4183a4ad6f130358ef64
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
 -/
 import Mathlib.Algebra.Group.Units
 

diff --git a/Mathlib/Algebra/Group/TypeTags.lean b/Mathlib/Algebra/Group/TypeTags.lean
@@ -2,6 +2,11 @@
 Copyright (c) 2018 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
+
+! This file was ported from Lean 3 source module algebra.group.type_tags
+! leanprover-community/mathlib commit 6eb334bd8f3433d5b08ba156b8ec3e6af47e1904
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
 -/
 import Mathlib.Algebra.Hom.Group
 import Mathlib.Logic.Equiv.Defs

diff --git a/Mathlib/Algebra/Group/ULift.lean b/Mathlib/Algebra/Group/ULift.lean
@@ -2,6 +2,11 @@
 Copyright (c) 2020 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
+
+! This file was ported from Lean 3 source module algebra.group.ulift
+! leanprover-community/mathlib commit 655994e298904d7e5bbd1e18c95defd7b543eb94
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
 -/
 import Mathlib.Data.Int.Cast.Defs
 import Mathlib.Algebra.Hom.Equiv.Basic

diff --git a/Mathlib/Algebra/Group/Units.lean b/Mathlib/Algebra/Group/Units.lean
@@ -2,6 +2,11 @@
 Copyright (c) 2017 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Mario Carneiro, Johannes Hölzl, Chris Hughes, Jens Wagemaker, Jon Eugster
+
+! This file was ported from Lean 3 source module algebra.group.units
+! leanprover-community/mathlib commit 0f601d095cdfe465edc51882323d19e6b333c419
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
 -/
 import Mathlib.Algebra.Group.Basic
 import Mathlib.Logic.Nontrivial

diff --git a/Mathlib/Algebra/Group/WithOne/Basic.lean b/Mathlib/Algebra/Group/WithOne/Basic.lean
@@ -2,6 +2,11 @@
 Copyright (c) 2018 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Johan Commelin
+
+! This file was ported from Lean 3 source module algebra.group.with_one.basic
+! leanprover-community/mathlib commit 4dc134b97a3de65ef2ed881f3513d56260971562
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
 -/
 import Mathlib.Algebra.Group.WithOne.Defs
 import Mathlib.Algebra.Hom.Equiv.Basic

diff --git a/Mathlib/Algebra/Group/WithOne/Defs.lean b/Mathlib/Algebra/Group/WithOne/Defs.lean
@@ -2,6 +2,11 @@
 Copyright (c) 2018 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Johan Commelin
+
+! This file was ported from Lean 3 source module algebra.group.with_one.defs
+! leanprover-community/mathlib commit e574b1a4e891376b0ef974b926da39e05da12a06
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
 -/
 import Mathlib.Order.WithBot
 import Mathlib.Algebra.Ring.Defs

diff --git a/Mathlib/Algebra/Group/WithOne/Units.lean b/Mathlib/Algebra/Group/WithOne/Units.lean
@@ -2,6 +2,11 @@
 Copyright (c) 2018 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Johan Commelin
+
+! This file was ported from Lean 3 source module algebra.group.with_one.units
+! leanprover-community/mathlib commit 4e87c8477c6c38b753f050bc9664b94ee859896c
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
 -/
 import Mathlib.Algebra.Group.WithOne.Basic
 import Mathlib.Algebra.GroupWithZero.Units.Basic

diff --git a/Mathlib/Algebra/GroupPower/Basic.lean b/Mathlib/Algebra/GroupPower/Basic.lean
@@ -2,6 +2,11 @@
 Copyright (c) 2015 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Robert Y. Lewis
+
+! This file was ported from Lean 3 source module algebra.group_power.basic
+! leanprover-community/mathlib commit 9b2660e1b25419042c8da10bf411aa3c67f14383
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
 -/
 import Mathlib.Algebra.Divisibility.Basic
 import Mathlib.Algebra.Group.Commute

diff --git a/Mathlib/Algebra/GroupPower/Identities.lean b/Mathlib/Algebra/GroupPower/Identities.lean
@@ -2,6 +2,11 @@
 Copyright (c) 2020 Bryan Gin-ge Chen. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bryan Gin-ge Chen, Kevin Lacker
+
+! This file was ported from Lean 3 source module algebra.group_power.identities
+! leanprover-community/mathlib commit c4658a649d216f57e99621708b09dcb3dcccbd23
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
 -/
 import Mathlib.Tactic.Ring
 

diff --git a/Mathlib/Algebra/GroupPower/Order.lean b/Mathlib/Algebra/GroupPower/Order.lean
@@ -2,6 +2,11 @@
 Copyright (c) 2015 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Robert Y. Lewis
+
+! This file was ported from Lean 3 source module algebra.group_power.order
+! leanprover-community/mathlib commit fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
 -/
 import Mathlib.Algebra.Order.Ring.Abs
 import Mathlib.Algebra.Order.WithZero

diff --git a/Mathlib/Algebra/GroupPower/Ring.lean b/Mathlib/Algebra/GroupPower/Ring.lean
@@ -3,6 +3,11 @@ Copyright (c) 2015 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Robert Y. Lewis
 Ported by: Joël Riou
+
+! This file was ported from Lean 3 source module algebra.group_power.ring
+! leanprover-community/mathlib commit fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
 -/
 
 import Mathlib.Algebra.GroupPower.Basic

diff --git a/Mathlib/Algebra/GroupWithZero/Basic.lean b/Mathlib/Algebra/GroupWithZero/Basic.lean
@@ -2,6 +2,11 @@
 Copyright (c) 2020 Johan Commelin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
+
+! This file was ported from Lean 3 source module algebra.group_with_zero.basic
+! leanprover-community/mathlib commit a148d797a1094ab554ad4183a4ad6f130358ef64
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
 -/
 
 import Mathlib.Algebra.Group.Basic

diff --git a/Mathlib/Algebra/GroupWithZero/Commute.lean b/Mathlib/Algebra/GroupWithZero/Commute.lean
@@ -2,6 +2,11 @@
 Copyright (c) 2020 Johan Commelin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
+
+! This file was ported from Lean 3 source module algebra.group_with_zero.commute
+! leanprover-community/mathlib commit 70d50ecfd4900dd6d328da39ab7ebd516abe4025
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
 -/
 import Mathlib.Algebra.GroupWithZero.Semiconj
 import Mathlib.Algebra.Group.Commute

diff --git a/Mathlib/Algebra/GroupWithZero/Defs.lean b/Mathlib/Algebra/GroupWithZero/Defs.lean
@@ -2,6 +2,11 @@
 Copyright (c) 2020 Johan Commelin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
+
+! This file was ported from Lean 3 source module algebra.group_with_zero.defs
+! leanprover-community/mathlib commit 2aa04f651209dc8f37b9937a8c4c20c79571ac52
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
 -/
 import Mathlib.Algebra.Group.Defs
 import Mathlib.Logic.Nontrivial

diff --git a/Mathlib/Algebra/GroupWithZero/Divisibility.lean b/Mathlib/Algebra/GroupWithZero/Divisibility.lean
@@ -3,6 +3,11 @@ Copyright (c) 2014 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Amelia Livingston, Yury Kudryashov,
 Neil Strickland, Aaron Anderson
+
+! This file was ported from Lean 3 source module algebra.group_with_zero.divisibility
+! leanprover-community/mathlib commit f1a2caaf51ef593799107fe9a8d5e411599f3996
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
 -/
 import Mathlib.Algebra.GroupWithZero.Basic
 import Mathlib.Algebra.Divisibility.Units