leanprover-community / leanprover-community/mathlib4
chore(FieldTheory/Finite): switch from Fintype to Finite/Nat.card
Nobody has claimed this yet.
- Dominant language
- Lean
- Stars
- 4.1k
- Forks
- 1.7k
- PR merge metrics
- No merged PRs in 30d
Description
like what @tb65536 has done for finite group theory in #6081, #13431, #13432, #13630, #13637, #14789, #14854, #14856, #19074.
The files in question:
https://github.com/leanprover-community/mathlib4/blob/f2bf11f4287d61b6fe50ea974ac1a849060e955e/Mathlib/FieldTheory/Finite/Basic.lean
https://github.com/leanprover-community/mathlib4/blob/f2bf11f4287d61b6fe50ea974ac1a849060e955e/Mathlib/FieldTheory/Finite/GaloisField.lean
possibly also MvPolynomial.R etc.
Requires Nat.card version of theorems like Module.card_eq_pow_finrank: here we only need to assume [Finite V], not [Finite K]. (Update: this particular lemma has been added in #24407.)
Contributor guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Research direction
Start by comparing the finite-group changes in issues #6081, #13431, #13432, #13630, #13637, #14789, #14854, #14856, and #19074. Read Mathlib/FieldTheory/Finite/Basic.lean and GaloisField.lean, then inspect MvPolynomial.R and the Nat.card form of Module.card_eq_pow_finrank. Done means the FieldTheory/Finite results use Finite/Nat.card consistently, including the required theorem assumptions.
Written by the indexing model from the issue text.
Assessment
- Domain
- devtools
- Issue type
- Refactor
- Difficulty
- 4/5
- Estimated time
- 3-5 days
- Activity status
- Stale
- Clarity
- Mostly clear
- Newbie friendliness
- 38/100