New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - chore: Make sure WithOne
doesn't import rings
#10275
Conversation
Reorder the `WithOne` material. `Algebra.Group.WithOne.Defs` was hiding a `Ring` import! I credit Johan and Mario for leanprover-community/mathlib#2707.
"Deconstruct an `x : WithZero α` to the underlying value in `α`, given a proof that `x ≠ 0`."] | ||
def unone {x : WithOne α} (hx : x ≠ 1) : α := | ||
WithBot.unbot x hx | ||
def unone : ∀ {x : WithOne α}, x ≠ 1 → α | (x : α), _ => x |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
What's the motivation for this change?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
You don't need to import WithBot
anymore. It's weird that WithBot
API was used in WithOne
API.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
bors d+
Thanks!
end WithZero | ||
|
||
-- Check that we haven't needed to import all the basic lemmas about groups, | ||
-- by asserting a random sample don't exist here: | ||
assert_not_exists inv_involutive | ||
assert_not_exists div_right_inj | ||
assert_not_exists pow_ite | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is on purpose: The comment above only applies to the three previous assert_not_exists
, not to this one.
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
Reorder the `WithOne` material. * `Algebra.Group.WithOne.Defs` was hiding a `Ring` import! I credit Johan and Mario for leanprover-community/mathlib#2707. * `WithBot` is not needed to define `WithOne.unone`. It's simpler to redefine it by hand. In the future, we might want to have an `Option` version (but not sure how much that's worth, since it would basically be `Option.get` again).
Pull request successfully merged into master. Build succeeded: |
WithOne
doesn't import ringsWithOne
doesn't import rings
Reorder the `WithOne` material. * `Algebra.Group.WithOne.Defs` was hiding a `Ring` import! I credit Johan and Mario for leanprover-community/mathlib#2707. * `WithBot` is not needed to define `WithOne.unone`. It's simpler to redefine it by hand. In the future, we might want to have an `Option` version (but not sure how much that's worth, since it would basically be `Option.get` again).
Reorder the
WithOne
material.Algebra.Group.WithOne.Defs
was hiding aRing
import! I credit Johan and Mario for [Merged by Bors] - refactor(algebra): merge init_.algebra into algebra mathlib#2707.WithBot
is not needed to defineWithOne.unone
. It's simpler to redefine it by hand. In the future, we might want to have anOption
version (but not sure how much that's worth, since it would basically beOption.get
again).