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

[Merged by Bors] - refactor(number_theory/padics/padic_norm): Switch nat and rat definitions #12454

Closed
wants to merge 61 commits into from
Closed

[Merged by Bors] - refactor(number_theory/padics/padic_norm): Switch nat and rat definitions #12454

wants to merge 61 commits into from

Conversation

BoltonBailey
Copy link
Collaborator

@BoltonBailey BoltonBailey commented Mar 5, 2022 •
edited
Loading

Switches the order in which padic_val_nat and padic_val_rat are defined.

This PR has also expanded to add padic_val_int and some API lemmas for that.

Open in Gitpod

@kim-em kim-em added the awaiting-author A reviewer has asked the author a question or requested changes label Mar 8, 2022
@BoltonBailey BoltonBailey added awaiting-CI The author would like to see what CI has to say before doing more work. and removed awaiting-author A reviewer has asked the author a question or requested changes labels Mar 10, 2022
jcommelin
jcommelin reviewed Mar 10, 2022
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Reformatting some docstrings to be a bit more economic with lines of code.

src/number_theory/padics/padic_norm.lean Outdated Show resolved Hide resolved
src/number_theory/padics/padic_norm.lean Outdated Show resolved Hide resolved
src/number_theory/padics/padic_norm.lean Outdated Show resolved Hide resolved
src/number_theory/padics/padic_norm.lean Outdated Show resolved Hide resolved
src/number_theory/padics/padic_norm.lean Outdated Show resolved Hide resolved
src/number_theory/padics/padic_norm.lean Outdated Show resolved Hide resolved
BoltonBailey and others added 8 commits March 10, 2022 13:11
@BoltonBailey @jcommelin
Update src/number_theory/padics/padic_norm.lean
9b3ba9f 
Co-authored-by: Johan Commelin <johan@commelin.net>
@BoltonBailey @jcommelin
Update src/number_theory/padics/padic_norm.lean
3b8f6d5 
Co-authored-by: Johan Commelin <johan@commelin.net>
@BoltonBailey @jcommelin
Update src/number_theory/padics/padic_norm.lean
f3be9eb 
Co-authored-by: Johan Commelin <johan@commelin.net>
@BoltonBailey @jcommelin
Update src/number_theory/padics/padic_norm.lean
85b0e8d 
Co-authored-by: Johan Commelin <johan@commelin.net>
@BoltonBailey @jcommelin
Update src/number_theory/padics/padic_norm.lean
ae586d5 
Co-authored-by: Johan Commelin <johan@commelin.net>
@BoltonBailey @jcommelin
Update src/number_theory/padics/padic_norm.lean
b0387aa 
Co-authored-by: Johan Commelin <johan@commelin.net>
@BoltonBailey
fix proof
9ded751
@BoltonBailey
Merge branch 'BoltonBailey/padic-val-nat-rat-switch' of github.com:le…
81ca3f3 
…anprover-community/mathlib into BoltonBailey/padic-val-nat-rat-switch
@BoltonBailey BoltonBailey mentioned this pull request Mar 10, 2022
Closed
3 tasks
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Mar 10, 2022
@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Mar 10, 2022
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Mar 10, 2022
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Apr 11, 2022
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Apr 13, 2022
@BoltonBailey BoltonBailey mentioned this pull request Apr 13, 2022
Closed
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Apr 13, 2022
@BoltonBailey BoltonBailey added awaiting-CI The author would like to see what CI has to say before doing more work. and removed awaiting-author A reviewer has asked the author a question or requested changes labels Apr 13, 2022
@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Apr 14, 2022
bors bot pushed a commit that referenced this pull request Apr 14, 2022
@BoltonBailey
feat(ring_theory/multiplicity): int.nat_abs (#13420)
9631a91 
Spinning off of #12454
@BoltonBailey
Copy link
Collaborator Author

BoltonBailey commented Apr 14, 2022 •
edited
Loading

There are still probably things that can be done to improve this file. Some ideas I have are

  1. 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
  2. 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.
  3. Perhaps we could do a better job of ordering lemmas, I think there are several padic_val_nat sections

However, I don't necessarily want to add any more structural changes to this PR.

@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Apr 14, 2022
@leanprover-community-bot-assistant
Copy link
Collaborator

This PR/issue depends on:

@BoltonBailey BoltonBailey added the awaiting-review The author would like community review of the PR label Apr 18, 2022
jcommelin
jcommelin approved these changes Apr 21, 2022
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks 🎉

bors merge

@leanprover-community-bot-assistant leanprover-community-bot-assistant added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Apr 21, 2022
bors bot pushed a commit that referenced this pull request Apr 21, 2022
@BoltonBailey
refactor(number_theory/padics/padic_norm): Switch nat and rat definit…
8261501 
…ions (#12454)

Switches the order in which `padic_val_nat` and `padic_val_rat` are defined.

This PR has also expanded to add `padic_val_int` and some API lemmas for that.
@bors
Copy link

bors bot commented Apr 21, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title refactor(number_theory/padics/padic_norm): Switch nat and rat definitions [Merged by Bors] - refactor(number_theory/padics/padic_norm): Switch nat and rat definitions Apr 21, 2022
@bors bors bot closed this Apr 21, 2022
@bors bors bot deleted the BoltonBailey/padic-val-nat-rat-switch branch April 21, 2022 14:17
Julian added a commit that referenced this pull request Apr 21, 2022
@Julian
Merge remote-tracking branch 'origin/master' into torsion-free-groups
eb3119e 
* origin/master: (394 commits)
  feat(data/set/[basic|prod]): make `×ˢ` bind more strongly, and define `mem.out` (#13422)
  feat(order/basic): Simple shortcut lemmas (#13421)
  chore(number_theory/dioph): Cleanup (#13403)
  feat(analysis/normed_space/exponential): ring homomorphisms are preserved by the exponential (#13402)
  feat(algebraic_geometry/projective_spectrum): degree zero part of a localized ring (#13398)
  feat(set_theory/cardinal): A set of cardinals is small iff it's bounded (#13373)
  feat(data/polynomial/{derivative, iterated_deriv}): reduce assumptions (#13368)
  feat(algebra/monoid_algebra/grading): Use the new graded_algebra API (#13360)
  feat(algebra/group/to_additive): let @[to_additive] mimic alias’s docstrings (#13330)
  feat(set_theory/cofinality): Basic fundamental sequences (#13326)
  feat(special_functions/pow): continuity of real to complex power (#13244)
  feat(group_theory/torsion): extension closedness, and torsion scalars in modules (#13172)
  feat(category_theory/path_category): canonical quotient of a path category (#13159)
  refactor(number_theory/padics/padic_norm): Switch nat and rat definitions (#12454)
  feat(analysis/normed): more lemmas about the sup norm on pi types and matrices (#13536)
  fix(category_theory/monoidal): improve hygiene in coherence tactic (#13507)
  feat(src/number_theory/cyclotomic/discriminant): add discr_prime_pow_ne_two (#13465)
  chore(algebra/group/type_tags): missing simp lemmas (#13553)
  feat(measure_theory): allow measurability to prove ae_strongly_measurable (#13427)
  refactor(algebra/hom/group): generalize a few lemmas to `monoid_hom_class` (#13447)
  chore(data/list/cycle): Add basic `simp` lemmas + minor golfing (#13533)
  feat(algebra/hom/non_unital_alg): introduce notation for non-unital algebra homomorphisms (#13470)
  chore(algebra/group/defs): Declare `field_simps` attribute earlier (#13543)
  feat(analysis/normed/normed_field): add `one_le_(nn)norm_one` for nontrivial normed rings (#13556)
  refactor(analysis/calculus/cont_diff): reorder the file (#13468)
  move(set_theory/*): Organize in folders (#13530)
  chore(number_theory/zsqrtd/basic): simplify le_total proof (#13555)
  feat(group_theory/perm/basic): Iterating a permutation is the same as taking a power (#13554)
  feat(data/real/sqrt): `sqrt x < y ↔ x < y^2` (#13546)
  feat(algebra/hom/group and *): introduce `mul_hom M N` notation `M →ₙ* N` (#13526)
  feat(group_theory/schreier): Schreier's lemma in terms of `group.fg` and `group.rank` (#13361)
  feat(linear_algebra/trace): dual_tensor_hom is an equivalence + basis-free characterization of the trace (#10372)
  feat(order/filter/basic): allow functions between different types in lemmas about [co]map by a constant function (#13542)
  feat(data/finset/basic): simp `to_finset_eq_empty` (#13531)
  feat(topology/algebra/algebra): ℚ-scalar multiplication is continuous (#13458)
  chore(model_theory/encoding): Improve the encoding of terms  (#13532)
  feat(topology/separation): Finite sets in T2 spaces (#12845)
  feat(analysis/inner_product_space/gram_schmidt_ortho): Gram-Schmidt Orthogonalization and Orthonormalization (#12857)
  chore(algebra/big_operators/fin): golf finset.prod_range (#13535)
  chore(analysis/normed_space/star): make an argument explicit (#13523)
  feat(*): `op_op_op_comm` lemmas (#13528)
  chore(data/real/nnreal): add commuted version of `nnreal.mul_finset_sup` (#13512)
  chore(*/matrix): order `m` and `n` alphabetically (#13510)
  feat(analysis/calculus/specific_functions): trivial extra lemmas (#13516)
  feat(analysis): lemmas about nnnorm and nndist (#13498)
  feat(data/int/basic): add lemma `int.abs_le_one_iff` (#13513)
  feat(category_theory/limits): add characteristic predicate for zero objects (#13511)
  feat(order/filter/n_ary): Add lemma equating map₂ to map on the product (#13490)
  fix(analysis/locally_convex/balanced_hull_core): minimize import (#13450)
  feat(order/cover): define `wcovby` (#13424)
  ...
@BoltonBailey BoltonBailey mentioned this pull request Apr 21, 2022
Open
4 tasks
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers

@MichaelStollBayreuth MichaelStollBayreuth MichaelStollBayreuth left review comments

@jcommelin jcommelin jcommelin approved these changes

Assignees
No one assigned
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
6 participants
@BoltonBailey @leanprover-community-bot-assistant @jcommelin @MichaelStollBayreuth @kim-em @bryangingechen