mathlib3
refactor: change notation for interval integrals
#19225

Closed

refactor: change notation for interval integrals #19225

urkud wants to merge 4 commits into master from YK-interval-integral

Snapshot

dc47ecaa

urkud added RFC

urkud added awaiting-review

urkud requested a review 2 years ago

github-actions added modifies-synchronized-file

Also change notation for interval average

7c5fb901

Drop type annotations

c3d84684

urkud commented on 2023-06-30

Update src/probability/strong_law.lean

4213dcc5

eric-wieser added not-too-late

urkud removed not-too-late

urkud added too-late

urkud closed this 1 year ago

urkud deleted the YK-interval-integral branch 1 year ago

Reviewers

No reviews

Assignees

No one assigned

Labels

RFC awaiting-review modifies-synchronized-file too-late

Milestone

No milestone