Skip to content

Commit 2f5831a

Browse files
committed
doc(Data/Finset/Defs): switch to more informative link (#39590)
After 79e17d0 `Basic.lean` does not contain any information about big operators. This PR changes the cross-link to `Defs.lean` that now contains the documentation about big oeprators.
1 parent f5e3cae commit 2f5831a

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

Mathlib/Data/Finset/Defs.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,7 @@ Finsets give a basic foundation for defining finite sums and products over types
3030
2. `∏ i ∈ (s : Finset α), f i`.
3131
3232
Lean refers to these operations as big operators.
33-
More information can be found in `Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean`.
33+
More information can be found in `Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean`.
3434
3535
Finsets are directly used to define fintypes in Lean.
3636
A `Fintype α` instance for a type `α` consists of a universal `Finset α` containing every term of

0 commit comments

Comments
 (0)