Skip to content

[Merged by Bors] - feat(Algebra/GroupWithZero): WithZero.exp_injective#27666

Closed
pechersky wants to merge 8 commits intoleanprover-community:masterfrom
pechersky:with-zero-exp-inj
Closed

[Merged by Bors] - feat(Algebra/GroupWithZero): WithZero.exp_injective#27666
pechersky wants to merge 8 commits intoleanprover-community:masterfrom
pechersky:with-zero-exp-inj

Conversation

@pechersky
Copy link
Copy Markdown
Contributor

@pechersky pechersky commented Jul 30, 2025 •
edited
Loading

@pechersky pechersky added easy < 20s of review time. See the lifecycle page for guidelines. t-algebra Algebra (groups, rings, fields, etc) labels Jul 30, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jul 30, 2025 •
edited
Loading

PR summary 6ae95cf158

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ exp_eq_one
+ exp_inj
+ exp_injective

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

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

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jul 30, 2025
@pechersky pechersky mentioned this pull request Jul 30, 2025
Closed
1 task
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Aug 5, 2025
@mathlib4-dependent-issues-bot
Copy link
Copy Markdown
Collaborator

mathlib4-dependent-issues-bot commented Aug 5, 2025

This PR/issue depends on:

@kckennylau
Copy link
Copy Markdown
Collaborator

kckennylau commented Aug 5, 2025

Could you also add this lemma to Line 375 (and remove @[simp] from exp_zero)?

@[simp] lemma exp_eq_one {x : M} : exp x = 1 ↔ x = 0 :=
  ⟨(exp_injective ·), (· ▸ rfl)⟩

@kckennylau kckennylau requested a review from YaelDillies August 5, 2025 21:01
@pechersky
exp_eq_one_iff
e26b5c7 
both can be simp, #lint didn't complain
YaelDillies
YaelDillies approved these changes Aug 6, 2025
View reviewed changes
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

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

Thanks!

maintainer delegate

@github-actions
Copy link
Copy Markdown

github-actions bot commented Aug 6, 2025

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

@ghost ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Aug 6, 2025
@kckennylau
Copy link
Copy Markdown
Collaborator

kckennylau commented Aug 6, 2025

ah, I suppose we still want simp on exp 0 because it's dsimp!

riccardobrasca
riccardobrasca approved these changes Aug 6, 2025
View reviewed changes
Copy link
Copy Markdown
Member

@riccardobrasca riccardobrasca 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 d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Aug 6, 2025

✌️ pechersky can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@ghost ghost added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Aug 6, 2025
@pechersky @riccardobrasca
Update Mathlib/Algebra/GroupWithZero/WithZero.lean
c9af919 
Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>
@pechersky
Copy link
Copy Markdown
Contributor Author

pechersky commented Aug 6, 2025

bors r+

mathlib-bors bot pushed a commit that referenced this pull request Aug 6, 2025
@pechersky
feat(Algebra/GroupWithZero): WithZero.exp_injective (#27666)
dba85ce 
Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Aug 6, 2025

This PR was included in a batch that successfully built, but then failed to merge into master (it was a non-fast-forward update). It will be automatically retried.

mathlib-bors bot pushed a commit that referenced this pull request Aug 6, 2025
@pechersky
feat(Algebra/GroupWithZero): WithZero.exp_injective (#27666)
0228751 
Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Aug 6, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Algebra/GroupWithZero): WithZero.exp_injective [Merged by Bors] - feat(Algebra/GroupWithZero): WithZero.exp_injective Aug 6, 2025
@mathlib-bors mathlib-bors bot closed this Aug 6, 2025
staroperator pushed a commit to staroperator/mathlib4 that referenced this pull request Aug 8, 2025
@pechersky @staroperator
feat(Algebra/GroupWithZero): WithZero.exp_injective (leanprover-commu…
3287295 
…nity#27666)

Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>
Paul-Lez pushed a commit to Paul-Lez/mathlib4 that referenced this pull request Aug 23, 2025
@pechersky @Paul-Lez
feat(Algebra/GroupWithZero): WithZero.exp_injective (leanprover-commu…
c419838 
…nity#27666)

Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>
Paul-Lez pushed a commit to Paul-Lez/mathlib4 that referenced this pull request Aug 23, 2025
@pechersky @Paul-Lez
feat(Algebra/GroupWithZero): WithZero.exp_injective (leanprover-commu…
3e0294c 
…nity#27666)

Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@YaelDillies YaelDillies YaelDillies approved these changes

@riccardobrasca riccardobrasca riccardobrasca approved these changes

+1 more reviewer

@kckennylau kckennylau kckennylau left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). easy < 20s of review time. See the lifecycle page for guidelines. t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@pechersky @mathlib4-dependent-issues-bot @kckennylau @YaelDillies @riccardobrasca