Skip to content

Actions: RemyDegenne/mathlib4

Actions

Run pre-commit and in-place update PR on push

Actions

Loading...
Loading

Show workflow options

Create status badge

Loading
218 workflow runs
218 workflow runs

Filter by Event

Filter by Status

Filter by Branch

Filter by Actor

minor Run pre-commit and in-place update PR on push #218: Commit 134658c pushed by RemyDegenne
25s RD_tendstoOfTendstoInMeasure
RD_tendstoOfTendstoInMeasure
25s
move lemma Run pre-commit and in-place update PR on push #217: Commit a044082 pushed by RemyDegenne
32s RD_tendstoOfTendstoInMeasure
RD_tendstoOfTendstoInMeasure
32s
fix merge Run pre-commit and in-place update PR on push #216: Commit 804c000 pushed by RemyDegenne
34s RD_tendstoOfTendstoInMeasure
RD_tendstoOfTendstoInMeasure
34s
review: names Run pre-commit and in-place update PR on push #215: Commit c31be1e pushed by RemyDegenne
32s RD_portmanteau
RD_portmanteau
32s
Merge branch 'master' into RD_fernique Run pre-commit and in-place update PR on push #214: Commit 70b554e pushed by RemyDegenne
21s RD_fernique
RD_fernique
21s
Merge branch 'master' into RD_tendstoOfTendstoInMeasure Run pre-commit and in-place update PR on push #213: Commit d172276 pushed by RemyDegenne
28s RD_tendstoOfTendstoInMeasure
RD_tendstoOfTendstoInMeasure
28s
fix merge Run pre-commit and in-place update PR on push #212: Commit 94a4325 pushed by RemyDegenne
23s RD_stopRefactor
RD_stopRefactor
23s
fix Run pre-commit and in-place update PR on push #211: Commit 5fca450 pushed by RemyDegenne
27s RD_stopRefactor
RD_stopRefactor
27s
Merge branch 'master' into RD_stopRefactor Run pre-commit and in-place update PR on push #210: Commit bd41fe3 pushed by RemyDegenne
23s RD_stopRefactor
RD_stopRefactor
23s
minor golf Run pre-commit and in-place update PR on push #209: Commit 5e4dd87 pushed by RemyDegenne
26s RD_egorov
RD_egorov
26s
use measurable distances Run pre-commit and in-place update PR on push #208: Commit d2913d5 pushed by RemyDegenne
32s RD_egorov
RD_egorov
32s
remove useless aux lemma Run pre-commit and in-place update PR on push #207: Commit 041ce12 pushed by RemyDegenne
25s RD_egorov
RD_egorov
25s
chore: generalize Egorov file to strongly measurable edist assumption Run pre-commit and in-place update PR on push #206: Commit bc0ec7b pushed by RemyDegenne
28s RD_egorov
RD_egorov
28s
feat: AEMeasurable.dist Run pre-commit and in-place update PR on push #205: Commit 5e01554 pushed by RemyDegenne
29s RD_aemeasurableDist
RD_aemeasurableDist
29s
feat: extension of a function to the closure of a submodule Run pre-commit and in-place update PR on push #204: Commit cccc5f8 pushed by RemyDegenne
33s RD_completionClosure
RD_completionClosure
33s
unused import Run pre-commit and in-place update PR on push #203: Commit e056ea6 pushed by RemyDegenne
27s RD_borelWithTop
RD_borelWithTop
27s
unused argument Run pre-commit and in-place update PR on push #202: Commit e3856ef pushed by RemyDegenne
25s RD_borelWithTop
RD_borelWithTop
25s
move lemma Run pre-commit and in-place update PR on push #201: Commit 984be87 pushed by RemyDegenne
23s RD_borelWithTop
RD_borelWithTop
23s
use untopD in coe_enat lemma; todo: move it Run pre-commit and in-place update PR on push #200: Commit 72de747 pushed by RemyDegenne
32s RD_borelWithTop
RD_borelWithTop
32s
Update Mathlib/MeasureTheory/Constructions/BorelSpace/WithTop.lean Run pre-commit and in-place update PR on push #199: Commit a5ccf63 pushed by RemyDegenne
28s RD_borelWithTop
RD_borelWithTop
28s
chore: generalize Adapted to dependent types Run pre-commit and in-place update PR on push #198: Commit 716f422 pushed by RemyDegenne
30s RD_adaptedDependent
RD_adaptedDependent
30s
doc: scoped Run pre-commit and in-place update PR on push #197: Commit 007b8a8 pushed by RemyDegenne
24s RD_indepNotation
RD_indepNotation
24s
fix Run pre-commit and in-place update PR on push #196: Commit d8f0d6a pushed by RemyDegenne
25s RD_stopRefactor
RD_stopRefactor
25s
Merge branch 'RD_borelWithTop' into RD_stopRefactor Run pre-commit and in-place update PR on push #195: Commit 0f6599d pushed by RemyDegenne
22s RD_stopRefactor
RD_stopRefactor
22s
minor Run pre-commit and in-place update PR on push #194: Commit 03181a0 pushed by RemyDegenne
21s RD_borelWithTop
RD_borelWithTop
21s