Skip to content

[Merged by Bors] - chore(NumberTheory/MulChar): deprecate IsNontrivial, fix isPrimitive#13878

Closed
loefflerd wants to merge 6 commits intomasterfrom
DL_mulchar_fixes
Closed

[Merged by Bors] - chore(NumberTheory/MulChar): deprecate IsNontrivial, fix isPrimitive#13878
loefflerd wants to merge 6 commits intomasterfrom
DL_mulchar_fixes

Conversation

@loefflerd
Copy link
Copy Markdown
Contributor

@loefflerd loefflerd commented Jun 16, 2024

  • Deprecate MulChar.IsNontrivial (following the analogous change for AddChar's a few days ago);
  • fix capitalisation of DirichletCharacter.isPrimitive;
  • adjust some lemmas to take a Nat argument with a NeZero instance, rather than a PNat, which is more general and flexible.

Open in Gitpod

github-actions[bot]
github-actions bot reviewed Jun 16, 2024
View reviewed changes
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 16, 2024 •
edited
Loading

PR summary fc593e9499

Import changes

No significant changes to the import graph

Declarations diff

+ IsPrimitive
+ eq_one_iff
+ injective_ringHomComp
+ ne_one_iff
+ primitive_mul_isPrimitive
+ quadraticChar_exists_neg_one'
+ quadraticChar_ne_one
+ ringHomComp_eq_one_iff
+ ringHomComp_ne_one_iff
+ sum_eq_zero_of_ne_one

You can run this locally as follows 
## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

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

@loefflerd loefflerd added awaiting-review t-number-theory Number theory (also use t-algebra or t-analysis to specialize) labels Jun 16, 2024
@loefflerd loefflerd mentioned this pull request Jun 16, 2024
Closed
4 tasks
@YaelDillies
Copy link
Copy Markdown
Contributor

YaelDillies commented Jun 16, 2024

Can you please make sure that PRs called feat contain new content? This is not the case of this one and, since it changes API in a trivial way (everything that could be done before can still be done after with a basically one to one correspondence), it should be chore (rather than refactor, which would involve changing definitions, refactoring the API...).

@loefflerd loefflerd changed the title feat(NumberTheory/MulChar): deprecate IsNontrivial, fix isPrimitive chore(NumberTheory/MulChar): deprecate IsNontrivial, fix isPrimitive Jun 16, 2024
@loefflerd
Copy link
Copy Markdown
Contributor Author

loefflerd commented Jun 16, 2024

Sure, sorry about that, fixed!

MichaelStollBayreuth
MichaelStollBayreuth reviewed Jun 16, 2024
View reviewed changes
MichaelStollBayreuth
MichaelStollBayreuth reviewed Jun 16, 2024
View reviewed changes
MichaelStollBayreuth
MichaelStollBayreuth reviewed Jun 16, 2024
View reviewed changes
MichaelStollBayreuth
MichaelStollBayreuth reviewed Jun 16, 2024
View reviewed changes
loefflerd and others added 2 commits June 16, 2024 20:48
@loefflerd @MichaelStollBayreuth
Apply suggestions from code review
bce76ce 
Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com>
@loefflerd
review changes
fc593e9
MichaelStollBayreuth
MichaelStollBayreuth approved these changes Jun 16, 2024
View reviewed changes
Copy link
Copy Markdown
Contributor

@MichaelStollBayreuth MichaelStollBayreuth left a comment

Choose a reason for hiding this comment

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

LGTM!

@MichaelStollBayreuth
Copy link
Copy Markdown
Contributor

MichaelStollBayreuth commented Jun 16, 2024

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 16, 2024

🚀 Pull request has been placed on the maintainer queue by MichaelStollBayreuth.

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jun 16, 2024
@riccardobrasca
Copy link
Copy Markdown
Member

riccardobrasca commented Jun 17, 2024

Thanks!

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jun 17, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jun 17, 2024
@loefflerd
chore(NumberTheory/MulChar): deprecate IsNontrivial, fix `isPrimiti…
78e130a 
…ve` (#13878)

- Deprecate `MulChar.IsNontrivial` (following the analogous change for `AddChar`'s a few days ago);
- fix capitalisation of `DirichletCharacter.isPrimitive`; 
- adjust some lemmas to take a `Nat` argument with a `NeZero` instance, rather than a `PNat`, which is more general and flexible.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 17, 2024

Build failed (retrying...):

mathlib-bors bot pushed a commit that referenced this pull request Jun 17, 2024
@loefflerd
chore(NumberTheory/MulChar): deprecate IsNontrivial, fix `isPrimiti…
e6faccc 
…ve` (#13878)

- Deprecate `MulChar.IsNontrivial` (following the analogous change for `AddChar`'s a few days ago);
- fix capitalisation of `DirichletCharacter.isPrimitive`; 
- adjust some lemmas to take a `Nat` argument with a `NeZero` instance, rather than a `PNat`, which is more general and flexible.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 17, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore(NumberTheory/MulChar): deprecate IsNontrivial, fix isPrimitive [Merged by Bors] - chore(NumberTheory/MulChar): deprecate IsNontrivial, fix isPrimitive Jun 17, 2024
@mathlib-bors mathlib-bors bot closed this Jun 17, 2024
@mathlib-bors mathlib-bors bot deleted the DL_mulchar_fixes branch June 17, 2024 11:31
AntoineChambert-Loir pushed a commit that referenced this pull request Jun 20, 2024
@loefflerd @AntoineChambert-Loir
chore(NumberTheory/MulChar): deprecate IsNontrivial, fix `isPrimiti…
90ea0c9 
…ve` (#13878)

- Deprecate `MulChar.IsNontrivial` (following the analogous change for `AddChar`'s a few days ago);
- fix capitalisation of `DirichletCharacter.isPrimitive`; 
- adjust some lemmas to take a `Nat` argument with a `NeZero` instance, rather than a `PNat`, which is more general and flexible.
kbuzzard pushed a commit that referenced this pull request Jun 26, 2024
@loefflerd @kbuzzard
chore(NumberTheory/MulChar): deprecate IsNontrivial, fix `isPrimiti…
4f7d8d2 
…ve` (#13878)

- Deprecate `MulChar.IsNontrivial` (following the analogous change for `AddChar`'s a few days ago);
- fix capitalisation of `DirichletCharacter.isPrimitive`; 
- adjust some lemmas to take a `Nat` argument with a `NeZero` instance, rather than a `PNat`, which is more general and flexible.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@github-actions github-actions[bot] github-actions[bot] left review comments

@MichaelStollBayreuth MichaelStollBayreuth MichaelStollBayreuth approved these changes

Assignees

@MichaelStollBayreuth MichaelStollBayreuth

Labels

maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. ready-to-merge This PR has been sent to bors. t-number-theory Number theory (also use t-algebra or t-analysis to specialize)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@loefflerd @YaelDillies @MichaelStollBayreuth @riccardobrasca