Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

padic_norm file maintenance #13574

Open
1 of 4 tasks
BoltonBailey opened this issue Apr 21, 2022 · 0 comments
Open
1 of 4 tasks

padic_norm file maintenance #13574

BoltonBailey opened this issue Apr 21, 2022 · 0 comments

Comments

@BoltonBailey
Copy link
Collaborator

BoltonBailey commented Apr 21, 2022

There are still probably things that can be done to improve the number_theory/padic_norm.lean. Some ideas:

  • Split the file in two at the definition padic_norm with that latter part being called padic_norm.lean and the first part being padic_val.lean. See [Merged by Bors] - refactor(number_theory/padics/padic_norm): split file #13576
  • There are a lot of lemmas with [prime p] typeclass argument which are actually only need something like p \ne 1. Perhaps some of these are useful, but they could be named more consistently.
  • Perhaps we could do a better job of ordering lemmas, I think there are several padic_val_nat sections.
  • As I think Michael Stoll suggested, it may be better to put the definition of padic_val_int before padic_val_nat.

Originally posted by @BoltonBailey in #12454 (comment)

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant