Skip to content

[Merged by Bors] - feat(Data/ZMod/IntUnitsPower): The power operator by ZMod 2 on ℤˣ#7661

Closed
eric-wieser wants to merge 4 commits intomasterfrom
eric-wieser/int-zmod-power
Closed

[Merged by Bors] - feat(Data/ZMod/IntUnitsPower): The power operator by ZMod 2 on ℤˣ#7661
eric-wieser wants to merge 4 commits intomasterfrom
eric-wieser/int-zmod-power

Conversation

@eric-wieser
Copy link
Copy Markdown
Member

@eric-wieser eric-wieser commented Oct 13, 2023 •
edited
Loading

@eric-wieser eric-wieser added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-algebra Algebra (groups, rings, fields, etc) labels Oct 13, 2023
@eric-wieser eric-wieser mentioned this pull request Oct 13, 2023
Closed
6 tasks
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Oct 13, 2023
riccardobrasca
riccardobrasca approved these changes Oct 23, 2023
View reviewed changes
Copy link
Copy Markdown
Member

@riccardobrasca riccardobrasca left a comment •
edited
Loading

Choose a reason for hiding this comment

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

Can you add

lemma z₂pow_sub (s : ℤˣ) (x y : ZMod 2) : s ^ (x - y) = s ^ x / s ^ y

If should hold if I am not too confused by subtraction and division.

bors d+

@bors
Copy link
Copy Markdown

bors bot commented Oct 23, 2023

✌️ eric-wieser 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 awaiting-review labels Oct 23, 2023
@eric-wieser
Copy link
Copy Markdown
Member Author

eric-wieser commented Oct 23, 2023

bors merge

I've added the lemma you requested, and added a TODO comment about further work.

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Oct 23, 2023
bors bot pushed a commit that referenced this pull request Oct 23, 2023
@eric-wieser
feat(Data/ZMod/IntUnitsPower): The power operator by ZMod 2 on ℤˣ (…
759f2af 
…#7661)

[Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Powers.20of.20.60.E2.84.A4.CB.A3.60.20by.20.60ZMod.202.60/near/396291926)
@eric-wieser eric-wieser mentioned this pull request Oct 23, 2023
Closed
2 tasks
@bors
Copy link
Copy Markdown

bors bot commented Oct 23, 2023

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title feat(Data/ZMod/IntUnitsPower): The power operator by ZMod 2 on ℤˣ [Merged by Bors] - feat(Data/ZMod/IntUnitsPower): The power operator by ZMod 2 on ℤˣ Oct 23, 2023
@bors bors bot closed this Oct 23, 2023
@bors bors bot deleted the eric-wieser/int-zmod-power branch October 23, 2023 15:34
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@riccardobrasca riccardobrasca riccardobrasca approved these changes

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@eric-wieser @riccardobrasca