Skip to content

Actions: leanprover-community/mathlib4

Actions

Post PR summary comment

Actions

Loading...
Loading

Show workflow options

Create status badge

Loading
PR_summary.yml
22,779 workflow runs
22,779 workflow runs

Filter by Event

Filter by Status

Filter by Branch

Filter by Actor

feat: setLintegral for indicator function and le_meas Post PR summary comment #22822: Pull request #15322 synchronize by urkud
October 9, 2024 19:20 51s integral.lebesgue
integral.lebesgue
October 9, 2024 19:20 51s
feat: Sym2-as-Finset theory Post PR summary comment #22821: Pull request #17587 synchronize by kmill
October 9, 2024 19:19 45s sym2_finset
sym2_finset
October 9, 2024 19:19 45s
chore: remove some variables Post PR summary comment #22820: Pull request #17592 opened by adomani
October 9, 2024 19:14 48s adomani/unused_vars8
adomani/unused_vars8
October 9, 2024 19:14 48s
feat(Measure/WithDensityFinite): redefine Measure.toFinite Post PR summary comment #22819: Pull request #17421 synchronize by urkud
October 9, 2024 19:07 51s YK-tofinite
YK-tofinite
October 9, 2024 19:07 51s
chore(Algebra/Order/GroupWithZero/Unbundled): deprecate useless lemmas, use ZeroLEOneClass Post PR summary comment #22818: Pull request #9250 synchronize by FR-vdash-bot
October 9, 2024 18:47 47s FR_order_refactor18
FR_order_refactor18
October 9, 2024 18:47 47s
feat(Analysis.InnerProductSpace): Decomposition of finite-dimensional inner product space as direct sum of joint eigenspaces of commuting finite tuples of symmetric operators Post PR summary comment #22817: Pull request #16569 synchronize by JonBannon
October 9, 2024 18:44 45s JointEigenspacesTuples
JointEigenspacesTuples
October 9, 2024 18:44 45s
feat(Probability/Kernel): the kernel Radon-Nikodym derivative and singular part are unique Post PR summary comment #22816: Pull request #17591 opened by RemyDegenne
October 9, 2024 18:35 1m 2s RD_krn
RD_krn
October 9, 2024 18:35 1m 2s
feat(Topology): define ContinuousEval{,Const} classes Post PR summary comment #22815: Pull request #17319 synchronize by urkud
October 9, 2024 18:16 52s YK-cont-eval
YK-cont-eval
October 9, 2024 18:16 52s
feat(CategoryTheory/KanExtensions): Evaluating lan twice amounts to taking a colimit Post PR summary comment #22814: Pull request #17531 synchronize by javra
October 9, 2024 18:08 1m 8s lanObjObjIsoColim
lanObjObjIsoColim
October 9, 2024 18:08 1m 8s
feat: Sym2-as-Finset theory Post PR summary comment #22813: Pull request #17587 synchronize by FordUniver
October 9, 2024 18:04 47s sym2_finset
sym2_finset
October 9, 2024 18:04 47s
fix: remove ToExpr Int instance Post PR summary comment #22812: Pull request #17590 opened by kmill
October 9, 2024 17:55 46s remove-toexpr-int
remove-toexpr-int
October 9, 2024 17:55 46s
feat (LocalRing/MaximalIdeal/Basic): add LocalRing.not_mem_maximalIdeal and nilradmax_localization_IsSelf Post PR summary comment #22811: Pull request #17549 synchronize by maddycrim
October 9, 2024 17:54 44s MC_localization
MC_localization
October 9, 2024 17:54 44s
chore: remove CovariantClass and ContravariantClass Post PR summary comment #22810: Pull request #13124 synchronize by FR-vdash-bot
October 9, 2024 17:51 1m 1s FR_mulmono
FR_mulmono
October 9, 2024 17:51 1m 1s
feat(NumberTheory/Ostrowski): First step of the proof of the Archimedean case of Ostrowski's Theorem Post PR summary comment #22809: Pull request #14442 synchronize by fbarroero
October 9, 2024 17:45 51s amos_ostrowski_arch
amos_ostrowski_arch
October 9, 2024 17:45 51s
feat: use aliases for CovariantClass α α (· * ·) (· ≤ ·) etc Post PR summary comment #22808: Pull request #13154 synchronize by FR-vdash-bot
October 9, 2024 17:44 49s FR_mulmono_alias
FR_mulmono_alias
October 9, 2024 17:44 49s
feat(NumberTheory/Ostrowski): First step of the proof of the Archimedean case of Ostrowski's Theorem Post PR summary comment #22807: Pull request #14442 synchronize by fbarroero
October 9, 2024 17:40 49s amos_ostrowski_arch
amos_ostrowski_arch
October 9, 2024 17:40 49s
feat(NumberTheory/Ostrowski): First step of the proof of the Archimedean case of Ostrowski's Theorem Post PR summary comment #22806: Pull request #14442 synchronize by fbarroero
October 9, 2024 17:39 49s amos_ostrowski_arch
amos_ostrowski_arch
October 9, 2024 17:39 49s
feat: use aliases for CovariantClass α α (· * ·) (· ≤ ·) etc Post PR summary comment #22805: Pull request #13154 synchronize by FR-vdash-bot
October 9, 2024 17:36 52s FR_mulmono_alias
FR_mulmono_alias
October 9, 2024 17:36 52s
feat(Topology): define ContinuousEval{,Const} classes Post PR summary comment #22804: Pull request #17319 synchronize by urkud
October 9, 2024 17:33 47s YK-cont-eval
YK-cont-eval
October 9, 2024 17:33 47s
feat (LocalRing/MaximalIdeal/Basic): add LocalRing.not_mem_maximalIdeal and nilradmax_localization_IsSelf Post PR summary comment #22803: Pull request #17549 synchronize by maddycrim
October 9, 2024 17:32 51s MC_localization
MC_localization
October 9, 2024 17:32 51s
refactor: migrate to dependent induction lemmas Post PR summary comment #22802: Pull request #17543 synchronize by j-loreaux
October 9, 2024 17:25 47s j-loreaux/induction-prime
j-loreaux/induction-prime
October 9, 2024 17:25 47s
perf: use implicit parameters in SMul hierarchy Post PR summary comment #22801: Pull request #17582 synchronize by FR-vdash-bot
October 9, 2024 17:22 47s FR_smul_instance2'
FR_smul_instance2'
October 9, 2024 17:22 47s
feat(Analysis/Normed/Group/Ultra): triangle ineq for tsum & tprod Post PR summary comment #22800: Pull request #17584 synchronize by loefflerd
October 9, 2024 17:22 45s DL_ultrametric_tsum
DL_ultrametric_tsum
October 9, 2024 17:22 45s
perf: use implicit parameters in SMul hierarchy Post PR summary comment #22799: Pull request #17582 synchronize by FR-vdash-bot
October 9, 2024 17:21 46s FR_smul_instance2'
FR_smul_instance2'
October 9, 2024 17:21 46s
feat: the multiGoal linter Post PR summary comment #22798: Pull request #12339 synchronize by adomani
October 9, 2024 16:55 50s adomani/lint_multiple_goals
adomani/lint_multiple_goals
October 9, 2024 16:55 50s