-
Notifications
You must be signed in to change notification settings - Fork 298
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] - feat(algebra/ordered_ring): more granular typeclasses for with_top α
and with_bot α
#7845
Conversation
`with_top α` now inherits the following typeclasses from `α` with suitable assumptions: * `mul_zero_one_class` * `semigroup_with_zero` * `monoid_with_zero` * `comm_monoid_with_zero` These were all split out of the existing `canonically_ordered_comm_semiring`, with their proofs unchanged. It is not possible to split further, as `distrib'` requires `add_eq_zero_iff`, and `canonically_ordered_comm_semiring` is the smallest typeclass that provides both this lemma and `mul_zero_class`.
with_top α
with_top α
and with_bot α
… ericwieser/nnreal_mul_actions
src/data/real/ereal.lean
Outdated
with_top.coe_mul.symm.trans $ | ||
with_bot.coe_eq_coe.mpr $ with_bot.mul_bot $ function.injective.ne (@option.some.inj _) h | ||
|
||
lemma to_real_mul : ∀ {x y : ereal} (hx : x ≠ ⊤) (h'x : x ≠ ⊥) (hy : y ≠ ⊤) (h'y : y ≠ ⊥), |
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.
I think this holds without any assumptions on x
or y
.
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.
I copied this lemma from the one about add
, but maybe you're right
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.
Good catch, I was able to remove all the assumptions.
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
…-community/mathlib into ericwieser/nnreal_mul_actions
bors r+ |
…` and `with_bot α` (#7845) `with_top α` and `with_bot α` now inherit the following typeclasses from `α` with suitable assumptions: * `mul_zero_one_class` * `semigroup_with_zero` * `monoid_with_zero` * `comm_monoid_with_zero` These were all split out of the existing `canonically_ordered_comm_semiring`, with their proofs unchanged. The same instances are added for `with_bot`. It is not possible to split further, as `distrib'` requires `add_eq_zero_iff`, and `canonically_ordered_comm_semiring` is the smallest typeclass that provides both this lemma and `mul_zero_class`. With these instances in place, we can now show `comm_monoid_with_zero ereal`.
Pull request successfully merged into master. Build succeeded: |
with_top α
and with_bot α
with_top α
and with_bot α
with_top α
andwith_bot α
now inherit the following typeclasses fromα
with suitable assumptions:mul_zero_one_class
semigroup_with_zero
monoid_with_zero
comm_monoid_with_zero
These were all split out of the existing
canonically_ordered_comm_semiring
, with their proofs unchanged.The same instances are added for
with_bot
.It is not possible to split further, as
distrib'
requiresadd_eq_zero_iff
, andcanonically_ordered_comm_semiring
is the smallest typeclass that provides both this lemma andmul_zero_class
.With these instances in place, we can now show
comm_monoid_with_zero ereal
.