Skip to content

Actions: leanprover-community/mathlib4

Actions

Label New Contributors

Actions

Loading...
Loading

Show workflow options

Create status badge

Loading
label_new_contributor.yml
55,393 workflow runs
55,393 workflow runs

Filter by Event

Filter by Status

Filter by Branch

Filter by Actor

feat: supremum of ≤ c ordinals of cardinal ≤ c has cardinal ≤ c Label New Contributors #114420: Pull request #37573 opened by vihdzp
11s
11s
doc(MeasureTheory): avoid lazy continuation lines Label New Contributors #114419: Pull request #37572 opened by harahu
10s
10s
doc(NumberTheory): avoid lazy continuation lines Label New Contributors #114418: Pull request #37571 opened by harahu
7s
7s
feat(Topology/Instances/AddCircle): add Ioc analogues of lift and equiv lemmas Label New Contributors #114417: Pull request #37570 opened by pitmonticone
11s
11s
feat: the Fuglede–Putnam–Rosenblum theorem for C⋆-algebras Label New Contributors #114416: Pull request #37569 opened by j-loreaux
11s
11s
[Merged by Bors] - feat(MeasureTheory/Integral/Bochner): add exists_ne_zero_of_integral_ne_zero and exists_ne_zero_of_setIntegral_ne_zero Label New Contributors #114415: Pull request #37568 opened by pitmonticone
10s
10s
doc(Analysis/DifferentialForm): fix equations in docstrings Label New Contributors #114414: Pull request #37567 opened by peabrainiac
10s
10s
doc(Order): avoid lazy continuation lines Label New Contributors #114413: Pull request #37566 opened by harahu
13s
13s
feat(Data/ENNReal): add ofReal_inv_le and ofReal_div_le Label New Contributors #114412: Pull request #37565 opened by pitmonticone
10s
10s
chore: bump toolchain to v4.30.0-rc1 Label New Contributors #114411: Pull request #37564 opened by Garmelon
8s
8s
feat(NumberTheory/ArithmeticFunction/LFunction): Euler products are multiplicative Label New Contributors #114410: Pull request #37563 opened by tb65536
8s
8s
feat(Combinatorics/SimpleGraph): add several lemmas about when Walk.bypass and Walk.cycleBypass do nothing Label New Contributors #114409: Pull request #37562 opened by IvanRenison
10s
10s
feat(Data/List): add lemma List.notMem_subset Label New Contributors #114408: Pull request #37561 opened by IvanRenison
10s
10s
feat(MeasureTheory/LpSpace): add ContinuousMap.memLp Label New Contributors #114407: Pull request #37560 opened by pitmonticone
10s
10s
feat(MeasureTheory/LpSeminorm): add HasCompactSupport.memLp_of_enorm_bound Label New Contributors #114406: Pull request #37559 opened by pitmonticone
8s
8s
[Merged by Bors] - feat(MeasureTheory/Integral/Lebesgue): add lintegral_eq_iSup_eapprox_lintegral' and lintegral_comp' Label New Contributors #114405: Pull request #37558 opened by pitmonticone
7s
7s
feat: Iic 2 = {0, 1, 2} Label New Contributors #114404: Pull request #37557 opened by vihdzp
9s
9s
feat(Topology/Order): Locale.localePointOfSpacePoint if we have a Scott Topology from an Algebraic DCPO Label New Contributors #114403: Pull request #37556 opened by edwin1729
34s
34s
feat(MeasureTheory/Integral/IntervalIntegral): weaken assumptions in trapezoidal_error_le Label New Contributors #114402: Pull request #37555 opened by yuanyi-350
7s
7s
[Merged by Bors] - chore: golf using positivity Label New Contributors #114401: Pull request #37554 opened by grunweg
13s
13s
Golf misc Label New Contributors #114400: Pull request #37553 opened by grunweg
11s
11s
feat(MeasureTheory/BorelSpace): add measurable_iSup_of_lowerSemicontinuous Label New Contributors #114399: Pull request #37552 opened by pitmonticone
11s
11s
feat(MeasureTheory/Integral/Average): add laverage_mono_ae and setLAverage_le_essSup Label New Contributors #114398: Pull request #37551 opened by pitmonticone
8s
8s
feat(Topology/Order): add nonempty_nhds_inter_Ioi Label New Contributors #114397: Pull request #37550 opened by pitmonticone
9s
9s
[Merged by Bors] - feat(Order/LiminfLimsup): add iSup_liminf_le_liminf_iSup Label New Contributors #114396: Pull request #37549 opened by pitmonticone
8s
8s