Skip to content

[Merged by Bors] - feat(AddChar): Various improvements#13579

Closed
YaelDillies wants to merge 2 commits intomasterfrom
add_char_qol_improvements
Closed

[Merged by Bors] - feat(AddChar): Various improvements#13579
YaelDillies wants to merge 2 commits intomasterfrom
add_char_qol_improvements

Conversation

@YaelDillies
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies commented Jun 6, 2024 •
edited by github-actions bot
Loading

  • Add a bunch of missing simp and norm_cast lemmas.
  • Get rid of IsNontrivial ψ since it's just ψ ≠ 1. This simplifies proofs.
  • Remove explicit arguments to toMonoidHomEquiv/toAddMonoidHomEquiv. We basically never need to provide them explicitly since unification usually does the job.

Open in Gitpod

@YaelDillies YaelDillies added blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) awaiting-review labels Jun 6, 2024
@mergify
Copy link
Copy Markdown

mergify bot commented Jun 6, 2024

⚠️ The sha of the head commit of this PR conflicts with #13576. Mergify cannot evaluate rules on this PR. ⚠️

2 similar comments
@mergify
Copy link
Copy Markdown

mergify bot commented Jun 6, 2024

⚠️ The sha of the head commit of this PR conflicts with #13576. Mergify cannot evaluate rules on this PR. ⚠️

@mergify
Copy link
Copy Markdown

mergify bot commented Jun 6, 2024

⚠️ The sha of the head commit of this PR conflicts with #13576. Mergify cannot evaluate rules on this PR. ⚠️

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 7, 2024

Import summary

No significant changes to the import graph

@ghost ghost removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jun 8, 2024
@ghost
Copy link
Copy Markdown

ghost commented Jun 8, 2024

This PR/issue depends on:

@YaelDillies YaelDillies force-pushed the add_char_qol_improvements branch from 527a63d to 1fbbf19 Compare June 8, 2024 09:13
@github-actions
Copy link
Copy Markdown

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

PR summary 342d5d1ff1

Import changes

No significant changes to the import graph

Declarations diff

+ IsPrimitive.of_ne_one
+ _root_.MonoidHom.compAddChar_apply
+ _root_.MonoidHom.compAddChar_injective_left
+ _root_.MonoidHom.compAddChar_injective_right
+ coe_mul
+ coe_one
+ coe_pow
+ coe_toAddMonoidHom
+ coe_toAddMonoidHomEquiv
+ coe_toAddMonoidHomEquiv_symm
+ coe_toMonoidHomEquiv
+ coe_toMonoidHomEquiv_symm
+ compAddMonoidHom_apply
+ compAddMonoidHom_injective_left
+ compAddMonoidHom_injective_right
+ eq_one_iff
+ injective_iff
+ map_sub_eq_div
+ ne_one_iff
+ sum_eq_card_of_eq_one
+ sum_eq_zero_of_ne_one
+ toAddMonoidHomEquiv_apply
+ toAddMonoidHomEquiv_symm_apply
+ toMonoidHomEquiv_apply
+ toMonoidHomEquiv_symm_apply
+ zmod_char_ne_one_iff
- IsNontrivial.isPrimitive
- sum_eq_card_of_is_trivial
- sum_eq_zero_of_isNontrivial
- zmod_char_isNontrivial_iff

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>

@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 10, 2024
@YaelDillies
feat(AddChar): Various improvements
b611888 
* Add a bunch of missing `simp` and `norm_cast` lemmas.
* Get rid of `IsNontrivial ψ` since it's just `ψ ≠ 1`. This simplifies proofs.
* Remove explicit arguments to `toMonoidHomEquiv`/`toAddMonoidHomEquiv`. We basically never need to provide them explicitly since unification usually does the job.
@YaelDillies YaelDillies force-pushed the add_char_qol_improvements branch from 1fbbf19 to b611888 Compare June 10, 2024 08:58
@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 10, 2024
@YaelDillies YaelDillies mentioned this pull request Jun 14, 2024
Closed
4 tasks
loefflerd
loefflerd reviewed Jun 14, 2024
View reviewed changes
Copy link
Copy Markdown
Contributor

@loefflerd loefflerd left a comment

Choose a reason for hiding this comment

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

This is definitely an improvement, thanks!

@loefflerd
Copy link
Copy Markdown
Contributor

loefflerd commented Jun 14, 2024

Looks good now, thanks!

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 14, 2024

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

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

riccardobrasca commented Jun 14, 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 14, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jun 14, 2024
@YaelDillies
feat(AddChar): Various improvements (#13579)
239c822 
* Add a bunch of missing `simp` and `norm_cast` lemmas.
* Get rid of `IsNontrivial ψ` since it's just `ψ ≠ 1`. This simplifies proofs.
* Remove explicit arguments to `toMonoidHomEquiv`/`toAddMonoidHomEquiv`. We basically never need to provide them explicitly since unification usually does the job.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 14, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(AddChar): Various improvements [Merged by Bors] - feat(AddChar): Various improvements Jun 14, 2024
@mathlib-bors mathlib-bors bot closed this Jun 14, 2024
@mathlib-bors mathlib-bors bot deleted the add_char_qol_improvements branch June 14, 2024 15:02
AntoineChambert-Loir pushed a commit that referenced this pull request Jun 20, 2024
@YaelDillies @AntoineChambert-Loir
feat(AddChar): Various improvements (#13579)
4b2dad8 
* Add a bunch of missing `simp` and `norm_cast` lemmas.
* Get rid of `IsNontrivial ψ` since it's just `ψ ≠ 1`. This simplifies proofs.
* Remove explicit arguments to `toMonoidHomEquiv`/`toAddMonoidHomEquiv`. We basically never need to provide them explicitly since unification usually does the job.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@loefflerd loefflerd loefflerd left review comments

@grunweg grunweg grunweg left review comments

Assignees

No one assigned

Labels

maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. ready-to-merge This PR has been sent to bors.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@YaelDillies @loefflerd @riccardobrasca @grunweg