Skip to content

Commit 602a93c

Browse files
committed
doc(Algebra): fix file refs (leanprover-community#33620)
Update some stale file references.
1 parent 95b16a2 commit 602a93c

5 files changed

Lines changed: 9 additions & 7 deletions

File tree

Mathlib/Algebra/Group/Subsemigroup/Operations.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -56,8 +56,8 @@ In this file we define various operations on `Subsemigroup`s and `MulHom`s.
5656
5757
### Implementation notes
5858
59-
This file follows closely `GroupTheory/Submonoid/Operations.lean`, omitting only that which is
60-
necessary.
59+
This file follows closely `Mathlib/Algebra/Group/Submonoid/Operations.lean`, omitting only that
60+
which is necessary.
6161
6262
## Tags
6363

Mathlib/Algebra/Group/Units/Defs.lean

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,8 @@ An element of a `Monoid` is a unit if it has a two-sided inverse.
1818
* `IsUnit x`: a predicate asserting that `x` is a unit (i.e., invertible element) of a monoid.
1919
2020
For both declarations, there is an additive counterpart: `AddUnits` and `IsAddUnit`.
21-
See also `Prime`, `Associated`, and `Irreducible` in `Mathlib/Algebra/Associated.lean`.
21+
See also `Prime`, `Associated`, and `Irreducible` in
22+
`Mathlib/Algebra/GroupWithZero/Associated.lean`.
2223
2324
## Notation
2425

Mathlib/Algebra/HierarchyDesign.lean

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -101,12 +101,13 @@ when applicable:
101101
instance Finsupp.Z [Z β] : Z (α →₀ β) := ...
102102
```
103103
* Instances transferred elementwise to `Set`s, like `Set.monoid`.
104-
See `Mathlib/Algebra/Pointwise.lean` for more examples.
104+
See `Mathlib/Algebra/Group/Pointwise/Set/Basic.lean` for more examples.
105105
```
106106
instance Set.Z [Z α] : Z (Set α) := ...
107107
```
108108
* Definitions for transferring the entire structure across an equivalence, like `Equiv.monoid`.
109-
See `Mathlib/Data/Equiv/TransferInstance.lean` for more examples. See also the `transport` tactic.
109+
See `Mathlib/Algebra/Group/TransferInstance.lean` for more examples. See also the `transport`
110+
tactic.
110111
```
111112
def Equiv.Z (e : α ≃ β) [Z β] : Z α := ...
112113
/-- When there is a new notion of `Z`-equiv: -/

Mathlib/Algebra/Module/Presentation/Differentials.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,7 @@ The main result in this file is that `Ω[S⁄R]` identifies to the quotient of t
2828
free `S`-module on `ι` by the submodule generated by these
2929
elements `pres.differentialsRelations.relation r`. We show this as a consequence
3030
of `Algebra.Extension.exact_cotangentComplex_toKaehler`
31-
from the file `Mathlib/RingTheory/Kaehler/CotangentComplex.lean`.
31+
from the file `Mathlib/RingTheory/Extension/Cotangent/Basic.lean`.
3232
3333
-/
3434

Mathlib/Algebra/Ring/Action/End.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ multiplication in `Equiv.Perm`, and multiplication in `CategoryTheory.End`, but
2020
`CategoryTheory.comp`.
2121
2222
This file is kept separate from `Mathlib/Algebra/Ring/Equiv.lean` so that
23-
`Mathlib/GroupTheory/Perm.lean` is free to use equivalences (and other files that use them) before
23+
`Mathlib/Data/Fintype/Perm.lean` is free to use equivalences (and other files that use them) before
2424
the group structure is defined.
2525
2626
## Tags

0 commit comments

Comments
 (0)