Skip to content

Actions: leanprover-community/mathlib4

Actions

Autolabel PRs

Actions

Loading...
Loading

Show workflow options

Create status badge

Loading
add_label_from_diff.yaml
2,500+ workflow runs
2,500+ workflow runs

Filter by Event

⌥ + click/return to exclude

Filter by Status

⌥ + click/return to exclude

Filter by Branch

⌥ + click/return to exclude

Filter by Actor

⌥ + click/return to exclude
feat(RingTheory): add lemmas about reesAlgebra Autolabel PRs #27746: Pull request #41556 opened by Thmoas-Guan
1m 22s
1m 22s
feat(Algebra/Order/Antidiagonal): connect Finset.HasAntidiagonal with Filter.TendstoCofinite Autolabel PRs #27745: Pull request #41555 opened by BryceT233
1m 20s
1m 20s
chore: remove noncomputable section when only theorems in file Autolabel PRs #27744: Pull request #41554 opened by felixpernegger
1m 20s
1m 20s
[Merged by Bors] - chore(CategoryTheory/Sites/Descent/Precoverage): deprecate duplicate theorem Autolabel PRs #27743: Pull request #41553 opened by tb65536
1m 30s
1m 30s
feat(Analysis/Calculus): monotonicity from nonnegative lower right Dini derivative outside a countable set Autolabel PRs #27742: Pull request #41552 opened by benjub
1m 19s
1m 19s
chore: no noncomputable inside noncomputable section Autolabel PRs #27741: Pull request #41551 opened by felixpernegger
1m 19s
1m 19s
chore(LinearAlgebra/TensorProduct/Map): add symm_lTensor and symm_rTensor Autolabel PRs #27740: Pull request #41550 opened by ScottCarnahan
1m 33s
1m 33s
feat: integral of EReal-valued functions Autolabel PRs #27739: Pull request #41549 opened by gaetanserre
1m 21s
1m 21s
chore: use to_dual for DedekindCut Autolabel PRs #27738: Pull request #41548 opened by JovanGerb
1m 22s
1m 22s
[Merged by Bors] - ci: run lake cache shadow pipeline with patched lake version with latest features Autolabel PRs #27737: Pull request #41547 opened by marcelolynch
1m 29s
1m 29s
feat: the product of vector measures Autolabel PRs #27736: Pull request #41546 opened by sgouezel
1m 21s
1m 21s
feat(RepresentationTheory/Homological/ContCohomology): add inflation maps in continuous cohomology Autolabel PRs #27735: Pull request #41545 opened by rmhi
1m 35s
1m 35s
refactor(Algebra/Polynomial): make coeff return a Finsupp Autolabel PRs #27734: Pull request #41544 opened by YaelDillies
1m 35s
1m 35s
refactor(NumberTheory): make InfinitePlace.Completion a one-field structure Autolabel PRs #27733: Pull request #41543 opened by smmercuri
1m 21s
1m 21s
refactor(AlgebraicGeometry/Sites/Small): golf and remove defeqs Autolabel PRs #27732: Pull request #41542 opened by tb65536
1m 19s
1m 19s
chore: prefer classical over open scoped Classical in proofs Autolabel PRs #27731: Pull request #41541 opened by felixpernegger
1m 21s
1m 21s
chore: rename arguments of Nat.strong_induction_on Autolabel PRs #27730: Pull request #41540 opened by plp127
1m 18s
1m 18s
chore(RepresentationTheory/Homological/ContCohomology): refactor functoriality Autolabel PRs #27729: Pull request #41539 opened by rmhi
1m 34s
1m 34s
feat(Algebra/Quaternion): quaternion are central simple Autolabel PRs #27728: Pull request #41538 opened by Mathias-Stout
1m 31s
1m 31s
feat(RingTheory/TwoSidedIdeal/Lattice): add lemmas on two-sided ideals Autolabel PRs #27727: Pull request #41537 opened by Mathias-Stout
1m 20s
1m 20s
chore(Algebra): make quaternion directory Autolabel PRs #27726: Pull request #41536 opened by Mathias-Stout
1m 31s
1m 31s
[Merged by Bors] - chore: move dualDistribEquiv Autolabel PRs #27725: Pull request #41535 opened by YaelDillies
1m 25s
1m 25s
feat(Geometry/Manifold): add ContMDiffConstSMul typeclass Autolabel PRs #27724: Pull request #41534 opened by qdiazblanco
20m 13s
20m 13s
refactor: notation for EventuallyEq on Set Autolabel PRs #27723: Pull request #41533 opened by YaelDillies
1m 28s
1m 28s
chore: remove all unneeded classical Autolabel PRs #27722: Pull request #41532 opened by felixpernegger
1m 29s
1m 29s