File tree Expand file tree Collapse file tree 4 files changed +11
-8
lines changed
Expand file tree Collapse file tree 4 files changed +11
-8
lines changed Original file line number Diff line number Diff line change @@ -17,8 +17,9 @@ In this file we continue the work on equivalences begun in `Mathlib/Logic/Equiv/
1717a lot of equivalences between various types and operations on these equivalences.
1818
1919More definitions of this kind can be found in other files.
20- E.g., `Mathlib/Algebra/Equiv/TransferInstance.lean` does it for many algebraic type classes like
21- `Group`, `Module`, etc.
20+ E.g., `Mathlib/Algebra/Group/TransferInstance.lean` does it for `Group`,
21+ `Mathlib/Algebra/Module/TransferInstance.lean` does it for `Module`, and similar files exist for
22+ other algebraic type classes.
2223
2324## Tags
2425
Original file line number Diff line number Diff line change @@ -22,7 +22,7 @@ In this file we define two types:
2222 not equality!) to express that various `Type`s or `Sort`s are equivalent.
2323
2424* `Equiv.Perm α`: the group of permutations `α ≃ α`. More lemmas about `Equiv.Perm` can be found in
25- `Mathlib/GroupTheory/Perm.lean `.
25+ `Mathlib/GroupTheory/Perm/ `.
2626
2727 Then we define
2828
@@ -45,8 +45,9 @@ Then we define
4545 - `Equiv.decidableEq` takes `e : α ≃ β` and `[DecidableEq β]` and returns `DecidableEq α`.
4646
4747 More definitions of this kind can be found in other files.
48- E.g., `Mathlib/Algebra/Equiv/TransferInstance.lean` does it for many algebraic type classes like
49- `Group`, `Module`, etc.
48+ E.g., `Mathlib/Algebra/Group/TransferInstance.lean` does it for `Group`,
49+ `Mathlib/Algebra/Module/TransferInstance.lean` does it for `Module`, and similar files exist for
50+ other algebraic type classes.
5051
5152 Many more such isomorphisms and operations are defined in `Mathlib/Logic/Equiv/Basic.lean`.
5253
Original file line number Diff line number Diff line change @@ -75,7 +75,7 @@ open Lean Meta Elab Tactic
7575/-! Implementation of the `mfld_set_tac` tactic for working with the domains of partially-defined
7676functions (`PartialEquiv`, `OpenPartialHomeomorph`, etc).
7777
78- This is in a separate file from `Mathlib/Logic/Equiv/MfldSimpsAttr .lean` because attributes need a
78+ This is in a separate file from `Mathlib/Tactic/Attr/Register .lean` because attributes need a
7979new file to become functional.
8080-/
8181
Original file line number Diff line number Diff line change @@ -24,8 +24,9 @@ In this file we continue the work on equivalences begun in `Mathlib/Logic/Equiv/
2424 satisfy the distributive law up to a canonical equivalence;
2525
2626 More definitions of this kind can be found in other files.
27- E.g., `Mathlib/Algebra/Equiv/TransferInstance.lean` does it for many algebraic type classes like
28- `Group`, `Module`, etc.
27+ E.g., `Mathlib/Algebra/Group/TransferInstance.lean` does it for `Group`,
28+ `Mathlib/Algebra/Module/TransferInstance.lean` does it for `Module`, and similar files exist for
29+ other algebraic type classes.
2930
3031## Tags
3132
You can’t perform that action at this time.
0 commit comments