File tree Expand file tree Collapse file tree 3 files changed +5
-5
lines changed
Expand file tree Collapse file tree 3 files changed +5
-5
lines changed Original file line number Diff line number Diff line change @@ -486,8 +486,8 @@ set_option backward.privateInPublic true in
486486`f(0) = nil`. For a nonzero word find the `D` that matches the initial `U`,
487487which has index `p.firstReturn`, then let `x` be everything strictly between said `U` and `D`,
488488and `y` be everything strictly after said `D`. `p = x.nest + y` with `x, y` (possibly empty)
489- Dyck words. `f(p) = f(x) △ f(y)`, where △ (defined in `Mathlib/Data/Tree.lean`) joins two subtrees
490- to a new root node. -/
489+ Dyck words. `f(p) = f(x) △ f(y)`, where △ (defined in `Mathlib/Data/Tree/Basic .lean`) joins two
490+ subtrees to a new root node. -/
491491private def equivTreeToFun (p : DyckWord) : Tree Unit :=
492492 if h : p = 0 then nil else
493493 have := semilength_insidePart_lt h
Original file line number Diff line number Diff line change @@ -36,12 +36,12 @@ both for itself and all its minors.
3636
3737It is not (provably) the case that all matroids are `InvariantCardinalRank`,
3838since the equicardinality of bases in general matroids is independent of ZFC
39- (see the module docstring of `Mathlib/Data /Matroid/Basic.lean`).
39+ (see the module docstring of `Mathlib/Combinatorics /Matroid/Basic.lean`).
4040Lemmas like `Matroid.Base.cardinalMk_diff_comm` become true for all matroids
4141only if they are weakened by replacing `Cardinal.mk` with the cruder `ℕ∞`-valued `Set.encard`.
4242The `ℕ∞`-valued rank and rank functions `Matroid.eRank` and `Matroid.eRk`,
4343which have a more unconditionally strong API,
44- are developed in `Mathlib/Data /Matroid/Rank/ENat.lean`.
44+ are developed in `Mathlib/Combinatorics /Matroid/Rank/ENat.lean`.
4545
4646## Implementation Details
4747
Original file line number Diff line number Diff line change @@ -46,7 +46,7 @@ which is why mathlib defines matroids using bases/independence. )
4646It is natural to ask if equicardinality of bases holds if 'cardinality' refers to
4747a term in `Cardinal` instead of `ℕ∞`, but the answer is that it doesn't.
4848The cardinal-valued rank functions `Matroid.cRank` and `Matroid.cRk` are defined in
49- `Mathlib/Data /Matroid/Rank/Cardinal.lean`, but have less desirable properties in general.
49+ `Mathlib/Combinatorics /Matroid/Rank/Cardinal.lean`, but have less desirable properties in general.
5050See the module docstring of that file for a discussion.
5151
5252## Implementation Details
You can’t perform that action at this time.
0 commit comments