Closed
Conversation
Collaborator
mo271
commented
Nov 4, 2023
Done by this commant on the `Mathlib` directory:
```
find . -type f -name '*.lean' -exec sed -i -E 's/(\[|, )←([A-Za-z])/\1← \2/g' {} +
```
find . -type f -name '*.lean' -exec sed -i -E 's/^( +)←([A-Za-z])/\1← \2/g' {} +
b5e744b to
3b1a427
Compare
Collaborator
Author
|
During the merge I removed one of two |
mo271
referenced
this pull request
Nov 5, 2023
…` and `Int` too (#7866) Instead of providing `instance : Pow ℤˣ (ZMod 2)`, this now provides `instance [Module R (Additive ℤˣ)] : Pow ℤˣ R`. It turns out that this instance already exists for `ℕ` and `ℤ`, so all we need to do is create `instance : Module (ZMod 2) (Additive ℤˣ)` and we obtain new definitions that generalize over all three types. As a result of the generalization, `z₂pow` has been renamed in lemmas to `uzpow` (`u`nits of `ℤ`). The motivation here is that I need $(-1) ^ i$ to make sense (and be lawful) for `ZMod 2` (on clifford algebras) and `ℕ` (on exterior algebras). [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/397569279)
964d90c to
50cc446
Compare
Collaborator
Author
Contributor
|
I don't think we should merge this given that there is no guideline and the |
12dc965 to
f8e0686
Compare
Contributor
|
Can we stop wasting time on this and worry about more important things? |
Collaborator
Author
The hope is to save everybody's time by agreeing on one style and use that. |
Contributor
|
bors r+ |
Contributor
|
Pull request successfully merged into master. Build succeeded: |
←←
awueth
pushed a commit
that referenced
this pull request
Dec 19, 2023
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.