Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit cc8c90d

Browse files
VierkantorVierkantor
committed
chore(data/equiv): split and move to logic/equiv (#12929)
Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Rearranging.20files.20in.20.60data.2F.60 This PR rearranges files in `data/equiv/` by 1) moving bundled isomorphisms to a relevant subfolder of `algebra/`; 2) moving `denumerable` and `encodable` to `logic/`; 3) moving the remainder of `data/equiv/` to `logic/equiv/`. The commits of this PR correspond to those steps. In particular, the following files were moved: * `data/equiv/module.lean` → `algebra/module/equiv.lean` * `data/equiv/mul_add.lean` → `algebra/hom/equiv.lean` * `data/equiv/mul_add_aut.lean` → `algebra/hom/aut.lean` * `data/equiv/ring.lean` → `algebra/ring/equiv.lean` * `data/equiv/ring_aut.lean` → `algebra/ring/aut.lean` * `data/equiv/denumerable.lean` → `logic/denumerable.lean` * `data/equiv/encodable/*.lean` → `logic/encodable/basic.lean logic/encodable/lattice.lean logic/encodable/small.lean` * `data/equiv/*.lean` to: `logic/equiv/basic.lean logic/equiv/fin.lean logic/equiv/functor.lean logic/equiv/local_equiv.lean logic/equiv/option.lean logic/equiv/transfer_instance.lean logic/equiv/embedding.lean logic/equiv/fintype.lean logic/equiv/list.lean logic/equiv/nat.lean logic/equiv/set.lean`
1 parent 434a938 commit cc8c90d

118 files changed

Lines changed: 148 additions & 148 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎src/algebra/algebra/basic.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Kenny Lau, Yury Kudryashov
55
-/
66
import algebra.module.basic
7+
import algebra.ring.aut
78
import linear_algebra.span
89
import tactic.abel
9-
import data.equiv.ring_aut
1010

1111
/-!
1212
# Algebras over commutative semirings

‎src/algebra/big_operators/basic.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,8 +5,8 @@ Authors: Johannes Hölzl
55
-/
66

77
import algebra.group.pi
8+
import algebra.hom.equiv
89
import algebra.ring.opposite
9-
import data.equiv.mul_add
1010
import data.finset.fold
1111
import data.fintype.basic
1212
import data.set.pairwise

‎src/algebra/category/CommRing/basic.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ Authors: Scott Morrison, Johannes Hölzl, Yury Kudryashov
55
-/
66
import algebra.category.Group.basic
77
import category_theory.concrete_category.reflects_isomorphisms
8-
import data.equiv.ring
8+
import algebra.ring.equiv
99

1010
/-!
1111
# Category instances for semiring, ring, comm_semiring, and comm_ring.

‎src/algebra/field_power.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Robert Y. Lewis
55
-/
66
import algebra.group_with_zero.power
7+
import algebra.ring.equiv
78
import tactic.linarith
8-
import data.equiv.ring
99

1010
/-!
1111
# Integer power operation on fields and division rings

‎src/algebra/free.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ Authors: Kenny Lau
66
import algebra.hom.group
77
import control.applicative
88
import control.traversable.basic
9-
import data.equiv.basic
9+
import logic.equiv.basic
1010

1111
/-!
1212
# Free constructions

‎src/algebra/group/conj.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,8 +5,8 @@ Authors: Patrick Massot, Chris Hughes, Michael Howes
55
-/
66
import algebra.group.semiconj
77
import algebra.group_with_zero.basic
8+
import algebra.hom.aut
89
import algebra.hom.group
9-
import data.equiv.mul_add_aut
1010
import data.fintype.basic
1111

1212
/-!

‎src/algebra/group/opposite.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,8 +5,8 @@ Authors: Kenny Lau
55
-/
66
import algebra.group.inj_surj
77
import algebra.group.commute
8+
import algebra.hom.equiv
89
import algebra.opposites
9-
import data.equiv.mul_add
1010

1111
/-!
1212
# Group structures on the multiplicative and additive opposites

‎src/algebra/group/type_tags.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Mario Carneiro
55
-/
66
import algebra.hom.group
7-
import data.equiv.basic
7+
import logic.equiv.basic
88
/-!
99
# Type tags that turn additive structures into multiplicative, and vice versa
1010

‎src/algebra/group/ulift.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2020 Scott Morrison. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Scott Morrison
55
-/
6-
import data.equiv.mul_add
6+
import algebra.hom.equiv
77

88
/-!
99
# `ulift` instances for groups and monoids

‎src/algebra/group/with_one.lean‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,10 +3,10 @@ Copyright (c) 2018 Mario Carneiro. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Mario Carneiro, Johan Commelin
55
-/
6+
import algebra.hom.equiv
67
import algebra.ring.basic
7-
import data.equiv.basic
8-
import data.equiv.mul_add
9-
import data.equiv.option
8+
import logic.equiv.basic
9+
import logic.equiv.option
1010

1111
/-!
1212
# Adjoining a zero/one to semigroups and related algebraic structures

0 commit comments

Comments
 (0)