-
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] - chore(measure_theory/measure_space): add missing finite_measure
instances
#8214
Conversation
JasonKYi
commented
Jul 6, 2021
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.
Looks reasonable, but this is not my area of expertise
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.
LGTM
@@ -435,6 +435,9 @@ instance : module ℝ≥0∞ (measure α) := | |||
injective.module ℝ≥0∞ ⟨to_outer_measure, zero_to_outer_measure, add_to_outer_measure⟩ | |||
to_outer_measure_injective smul_to_outer_measure | |||
|
|||
@[simp, norm_cast] theorem coe_nnreal_smul (c : ℝ≥0) (μ : measure α) : ⇑(c • μ) = c • μ := |
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.
Could you add a specific type ascription here? I don't know whether this is (c • μ : outer_measure α)
or (c • μ : α -> ennreal)
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.
Oh, it is the coe_to_fun
arrow. Still I'd appreciate the explicit typing.
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.
The current spelling matches the statement of coe_smul
a few lines above, and in various places throughout mathlib.
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.
Ok, never mind then
bors merge
Pull request successfully merged into master. Build succeeded: |
finite_measure
instancesfinite_measure
instances