feat(Mathlib.Data.Ordering.Dickson): Dickson orders

[AntoineChambert-Loir]

Dickson orders are a particular class of well founded orders
characterized by the fact that every nonempty set has finitely many minimal elements.
They appear in the classical theory of Groebner bases because it is easier to prove
that some sets are well founded using this property.

WiP. In the tfae function, property 2 is exactly Set.PartiallyWellOrderedOn, so the PR should be rewritten so as to use that property (and not define IsDickson).

---

[github-actions]

PR summary 04ce7fcd5d

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Data.Ordering.Dickson	748

---

Declarations diff

+ Equiv.isDickson_of_monotone
+ Fin.isDickson_nat
+ Finsupp.isDickson
+ Finsupp.isDickson_equiv
+ Finsupp.isDickson_nat
+ Nat.isDickson
+ Preorder.isDickson
+ Set.isBasis
+ WellFoundedLT.isDickson
+ exists_lt_and_le_of_isDickson
+ isDickson.wf
+ isDickson_iff_exists_monotone
+ isDickson_of_minimal_ne_and_finite
+ isDickson_prod
+ isDickson_tfae
+ minimal_ne_and_finite_of
+ wellFounded_iff_not_exists

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[b-mehta]

This looks exactly like the definition of a partially well-ordered set. Indeed, this part of the tfae exactly matches a special case of PartiallyWellOrderedOn. What do you need from this definition that isn't already part of the existing one?

[AntoineChambert-Loir]

For assumption 3, it's not that this set is finite, but that the equivalence classes (for the associated partial order) are finite. And when I proved that, I didn't think how to formalize the partial order associated to a preorder, or whether it already exists.

[b-mehta]

I'm afraid I don't quite follow. What's assumption 3? Could you also explain why this definition is different from PartiallyWellOrderedOn? It looks to me like you've proved it's a special case of that, on this line.

[b-mehta]

In particular, this tfae gives you exactly the statement that isDickson α is equivalent to PartiallyWellOrderedOn Set.univ (· ≤ ·), except that the latter is defined in greater generality. Additionally, using the API already given there gives you isDickson_iff_exists_monotone directly, instead of needing to write another proof.

[AntoineChambert-Loir]

The general theorem proves the equivalence of three analogous properties for a preorder : being Dickson, property 2, and a variant of property 3 which I can't state in Lean but that asserts the corresponding finiteness property in the partial order associated with the preorder.

[AntoineChambert-Loir]

Said otherwise : consider a preorder X and the partial order Y deduced from X. By definition, being Dickson is equivalent for X and Y, properties 1 and 2 are equivalent as well (because they involve only the strict relation), but property 3 is not. And it is for Y that it is equivalent to being Dickson.

[AntoineChambert-Loir]

So if somebody really needs Dickson preorders, they could just prove the equivalence with being Dickson for the associated partial order, and apply the already proved theorem.

[b-mehta]

So if somebody really needs Dickson preorders, they could just prove the equivalence with being Dickson for the associated partial order, and apply the already proved theorem.

Dickson preorders, and Dickson partial orders are already in mathlib however. This PR duplicates the definition, proves it is equivalent to the existing one, and re-proves lemmas which are already in mathlib. I'm afraid I still don't understand why it is useful to re-make the API, could you clarify?

[joneugster]

Mathlib has moved to PRs from forks. This PR is still from a branch of the main repository and will soon be closed! Please migrate the content to a fork and reopen a PR from there if you wish to do so. See Zulip topic for more instructions. Thank you for contributing to mathlib!

[mathlib-bors]

This pull request is now in draft mode. No active bors state needed cleanup.

While this PR remains draft, bors will ignore commands on this PR. Mark it ready for review before using commands like bors r+ or bors try.

[AntoineChambert-Loir]

This PR has been migrated to a fork-based workflow: #43969