-
Notifications
You must be signed in to change notification settings - Fork 297
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(analysis/seminorm): Add has_add
and has_scalar nnreal
#11414
Conversation
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
has_add
and has_scalar nnreal
has_add
and has_scalar nnreal
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@YaelDillies I stole your two lines for showing the |
As you want, but it's really not much. |
src/analysis/seminorm.lean
Outdated
fun_like.coe_injective.add_monoid_smul _ rfl coe_add (λ p n, coe_smul n p) | ||
|
||
instance : ordered_cancel_add_comm_monoid (seminorm 𝕜 E) := | ||
fun_like.coe_injective.ordered_cancel_add_comm_monoid _ rfl coe_add |
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.
Unfortunately this now forms a diamond with the instance above it. You need something like:
fun_like.coe_injective.ordered_cancel_add_comm_monoid _ rfl coe_add | |
{ nsmul := (•), | |
..seminorm.add_monoid, | |
..fun_like.coe_injective.ordered_cancel_add_comm_monoid _ rfl coe_add } |
You might have to fight lean a little to make it accept that.
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 compiles, but I don't know enough about how this instancing stuff works to judge whether it gets rid of the diamond:
def ordered_cancel_add_comm_monoid_aux : ordered_cancel_add_comm_monoid (seminorm 𝕜 E) :=
fun_like.coe_injective.ordered_cancel_add_comm_monoid _ rfl coe_add
instance : ordered_cancel_add_comm_monoid (seminorm 𝕜 E) :=
{nsmul := (•), ..seminorm.add_monoid, ..seminorm.ordered_cancel_add_comm_monoid_aux }
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.
That works, but you don't need the auxiliary definition. I pushed a commit.
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.
thank you. By the way, where are instances for stuff like mul_action (E → ℝ)
?
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.
They're in group_theory.group_action.pi
, I think. The instance in question is pi.mul_action
.
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!
✌️ mcdoll can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
Add instances of `has_add` and `has_scalar nnreal` type classes for `seminorm`. Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Pull request successfully merged into master. Build succeeded: |
has_add
and has_scalar nnreal
has_add
and has_scalar nnreal
…12624) Move `balanced`, `absorbs`, `absorbent` to a new file. For `analysis.seminorm`, I'm crediting * Jean for #4827 * myself for * #9097 * #11487 * Moritz for * #11329 * #11414 * #11477 For `analysis.locally_convex.basic`, I'm crediting * Jean for #4827 * Bhavik for * #7358 * #9097 * myself for * #9097 * #10999 * #11487
…12624) Move `balanced`, `absorbs`, `absorbent` to a new file. For `analysis.seminorm`, I'm crediting * Jean for #4827 * myself for * #9097 * #11487 * Moritz for * #11329 * #11414 * #11477 For `analysis.locally_convex.basic`, I'm crediting * Jean for #4827 * Bhavik for * #7358 * #9097 * myself for * #9097 * #10999 * #11487
Add instances of
has_add
andhas_scalar nnreal
type classes forseminorm
.Co-authored-by: Eric Wieser wieser.eric@gmail.com
I will do the additional structure in a second PR (after #11329 is merged).