Skip to content

Commit a30c9c0

Browse files
committed
doc(GroupTheory): fix file refs (leanprover-community#33305)
Fix some stale documentation file refs.
1 parent a39c234 commit a30c9c0

7 files changed

Lines changed: 9 additions & 8 deletions

File tree

Mathlib/GroupTheory/Abelianization/Defs.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ public import Mathlib.GroupTheory.Commutator.Basic
1212
1313
This file defines the commutator and the abelianization of a group. It furthermore prepares for the
1414
result that the abelianization is left adjoint to the forgetful functor from abelian groups to
15-
groups, which can be found in `Mathlib/Algebra/Category/GrpCat/Adjunctions.lean`.
15+
groups, which can be found in `Mathlib/Algebra/Category/Grp/Adjunctions.lean`.
1616
1717
## Main definitions
1818

Mathlib/GroupTheory/FreeAbelianGroup.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,7 @@ under pointwise addition. In this file, it is defined as the abelianisation
2222
of the free group on `α`. All the constructions and theorems required to show
2323
the adjointness of the construction and the forgetful functor are proved in this
2424
file, but the category-theoretic adjunction statement is in
25-
`Mathlib/Algebra/Category/GrpCat/Adjunctions.lean`.
25+
`Mathlib/Algebra/Category/Grp/Adjunctions.lean`.
2626
2727
## Main definitions
2828

Mathlib/GroupTheory/FreeGroup/Basic.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ public import Mathlib.Algebra.BigOperators.Group.List.Basic
1616
1717
This file defines free groups over a type. Furthermore, it is shown that the free group construction
1818
is an instance of a monad. For the result that `FreeGroup` is the left adjoint to the forgetful
19-
functor from groups to types, see `Mathlib/Algebra/Category/GrpCat/Adjunctions.lean`.
19+
functor from groups to types, see `Mathlib/Algebra/Category/Grp/Adjunctions.lean`.
2020
2121
## Main definitions
2222

Mathlib/GroupTheory/GroupAction/DomAct/ActionHom.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ into a separate file, not with the definition of `DomMulAct`.
1616
1717
## TODO
1818
19-
Add left actions of, e.g., `M` on `α →[N] β` to `Mathlib/Algebra/Hom/GroupAction.lean` and
19+
Add left actions of, e.g., `M` on `α →[N] β` to `Mathlib/Algebra/Group/Action/Hom.lean` and
2020
`SMulCommClass` instances saying that left and right actions commute.
2121
-/
2222

Mathlib/GroupTheory/GroupExtension/Defs.lean

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,8 @@ If `N` is abelian,
4646
4747
- there is a bijection between `N`-conjugacy classes of
4848
`(SemidirectProduct.toGroupExtension φ).Splitting` and `groupCohomology.H1`
49-
(which will be available in `GroupTheory/GroupExtension/Abelian.lean` to be added in a later PR).
49+
(which will be available in the planned file `Mathlib/GroupTheory/GroupExtension/Abelian.lean` to
50+
be added in a later PR).
5051
- there is a bijection between equivalence classes of group extensions and `groupCohomology.H2`
5152
(which is also stated as a TODO in `Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean`).
5253
-/

Mathlib/GroupTheory/Perm/Sign.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@ public import Mathlib.Data.Finset.Sigma
2525
The main definition of this file is `Equiv.Perm.sign`,
2626
associating a `ℤˣ` sign with a permutation.
2727
28-
Other lemmas have been moved to `Mathlib/GroupTheory/Perm/Fintype.lean`
28+
Other lemmas have been moved to `Mathlib/GroupTheory/Perm/Finite.lean`
2929
3030
-/
3131

Mathlib/GroupTheory/Submonoid/Inverses.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -20,8 +20,8 @@ For the pointwise inverse of submonoids of groups, please refer to the file
2020
`Mathlib/Algebra/Group/Submonoid/Pointwise.lean`.
2121
2222
`N.leftInv` is distinct from `N.units`, which is the subgroup of `Mˣ` containing all units that are
23-
in `N`. See the implementation notes of `Mathlib/GroupTheory/Submonoid/Units.lean` for more details
24-
on related constructions.
23+
in `N`. See the implementation notes of `Mathlib/Algebra/Group/Submonoid/Units.lean` for more
24+
details on related constructions.
2525
2626
## TODO
2727

0 commit comments

Comments
 (0)