mathlib3
feat(measure_theory/arithmetic): add instances on `subtype measurable`
#7833

Open

feat(measure_theory/arithmetic): add instances on `subtype measurable` #7833

eric-wieser wants to merge 2 commits into master from eric-wieser/measurable_subtype

feat(measure_theory/arithmetic): add instances on `subtype measurable`

20fafdad

eric-wieser added RFC

eric-wieser commented on 2021-06-10

Update src/measure_theory/arithmetic.lean

e2f411f1

github-actions added merge-conflict

RemyDegenne added t-measure-probability

kim-em added too-late

eric-wieser requested a review 2 years ago

Reviewers

No reviews

Assignees

No one assigned

Labels

RFC merge-conflict t-measure-probability too-late

Milestone

No milestone