Skip to content

Actions: leanprover-community/mathlib4

Add "ready-to-merge" and "delegated" label from comment

Actions

Loading...
Loading

Show workflow options

Create status badge

Loading
47,380 workflow runs
47,380 workflow runs

Filter by Event

Filter by Status

Filter by Branch

Filter by Actor

refactor (NumberTheory/ModularForms, Analysis/Complex/UpperHalfPlane) Refactor and clean up coercions
Add "ready-to-merge" and "delegated" label from comment #62595: Issue comment #18385 (comment) created by mathlib-bors bot
October 31, 2024 13:28 2s
October 31, 2024 13:28 2s
refactor: require that the range of a model with corners is included in the closure of its interior
Add "ready-to-merge" and "delegated" label from comment #62594: Issue comment #18403 (comment) created by mathlib-bors bot
October 31, 2024 13:21 3s
October 31, 2024 13:21 3s
refactor: require that the range of a model with corners is included in the closure of its interior
Add "ready-to-merge" and "delegated" label from comment #62593: Issue comment #18403 (comment) created by fpvandoorn
October 31, 2024 13:21 10s
October 31, 2024 13:21 10s
refactor: move slim_check to plausible
Add "ready-to-merge" and "delegated" label from comment #62592: Issue comment #18459 (comment) created by eric-wieser
October 31, 2024 12:40 2s
October 31, 2024 12:40 2s
refactor: require that the range of a model with corners is included in the closure of its interior
Add "ready-to-merge" and "delegated" label from comment #62591: Issue comment #18403 (comment) created by sgouezel
October 31, 2024 12:34 2s
October 31, 2024 12:34 2s
[Merged by Bors] - feat: add deprecation script
Add "ready-to-merge" and "delegated" label from comment #62590: Issue comment #18150 (comment) created by mathlib-bors bot
October 31, 2024 12:14 2s
October 31, 2024 12:14 2s
feat: add Dockerfiles for lean and mathlib
Add "ready-to-merge" and "delegated" label from comment #62589: Issue comment #15936 (comment) created by bryangingechen
October 31, 2024 12:13 2s
October 31, 2024 12:13 2s
[Merged by Bors] - feat: add deprecation script
Add "ready-to-merge" and "delegated" label from comment #62588: Issue comment #18150 (comment) created by adomani
October 31, 2024 12:07 13s
October 31, 2024 12:07 13s
chore(SetTheory/Ordinal/CantorNormalForm): CNF.exponents and CNF.coeffs
Add "ready-to-merge" and "delegated" label from comment #62587: Issue comment #15915 (comment) created by mathlib4-dependent-issues-bot
October 31, 2024 11:48 2s
October 31, 2024 11:48 2s
[Merged by Bors] - chore(SetTheory/Ordinal/CantorNormalForm): cleanup proofs
Add "ready-to-merge" and "delegated" label from comment #62586: Issue comment #16998 (comment) created by mathlib-bors bot
October 31, 2024 11:13 2s
October 31, 2024 11:13 2s
chore(CategoryTheory/Sites): make Subcanonical a class
Add "ready-to-merge" and "delegated" label from comment #62585: Issue comment #18186 (comment) created by dagurtomas
October 31, 2024 11:04 3s
October 31, 2024 11:04 3s
chore(CategoryTheory/Sites): make Subcanonical a class
Add "ready-to-merge" and "delegated" label from comment #62584: Issue comment #18186 (comment) created by leanprover-bot
October 31, 2024 11:00 3s
October 31, 2024 11:00 3s
chore(Order/Interval/Set/Infinite): instance NoMaxOrder.infinite and NoMinOrder.infinite
Add "ready-to-merge" and "delegated" label from comment #62583: Issue comment #18456 (comment) created by mathlib-bors bot
October 31, 2024 10:56 2s
October 31, 2024 10:56 2s
chore(Order/Interval/Set/Infinite): instance NoMaxOrder.infinite and NoMinOrder.infinite
Add "ready-to-merge" and "delegated" label from comment #62582: Issue comment #18456 (comment) created by Vierkantor
October 31, 2024 10:56 10s
October 31, 2024 10:56 10s
chore(ContinuousLinearMapWOT): generalize and golf
Add "ready-to-merge" and "delegated" label from comment #62581: Issue comment #17492 (comment) created by ADedecker
October 31, 2024 10:48 2s
October 31, 2024 10:48 2s
feat(Integral/Pi): a version of polarCoord for pi integrals
Add "ready-to-merge" and "delegated" label from comment #62580: Issue comment #18400 (comment) created by mathlib4-dependent-issues-bot
October 31, 2024 10:35 2s
October 31, 2024 10:35 2s
feat: quantales
Add "ready-to-merge" and "delegated" label from comment #62579: Issue comment #17289 (comment) created by PieterCuijpers
October 31, 2024 10:34 3s
October 31, 2024 10:34 3s
chore(CategoryTheory/Sites): make Subcanonical a class
Add "ready-to-merge" and "delegated" label from comment #62578: Issue comment #18186 (comment) created by dagurtomas
October 31, 2024 10:33 3s
October 31, 2024 10:33 3s
[Merged by Bors] - feat(NumberField/FundamentalCone): generalize the bijection to integral ideals
Add "ready-to-merge" and "delegated" label from comment #62577: Issue comment #18248 (comment) created by mathlib-bors bot
October 31, 2024 10:26 2s
October 31, 2024 10:26 2s
[Merged by Bors] - feat(NumberField/FundamentalCone): generalize the bijection to integral ideals
Add "ready-to-merge" and "delegated" label from comment #62576: Issue comment #18248 (comment) created by riccardobrasca
October 31, 2024 10:17 15s
October 31, 2024 10:17 15s
Feat: projective line over ℝ is homeomorphic to the one-point compactification of ℝ
Add "ready-to-merge" and "delegated" label from comment #62575: Issue comment #18306 (comment) created by ocfnash
October 31, 2024 10:03 2s
October 31, 2024 10:03 2s
[Merged by Bors] - feat(LinearAlgebra): nilpotent <-> charpoly = X ^ n
Add "ready-to-merge" and "delegated" label from comment #62574: Issue comment #18417 (comment) created by mathlib-bors bot
October 31, 2024 10:01 2s
October 31, 2024 10:01 2s
[Merged by Bors] - chore(Order/InitialSeg): private / delete inner workings
Add "ready-to-merge" and "delegated" label from comment #62573: Issue comment #17609 (comment) created by mathlib-bors bot
October 31, 2024 09:53 2s
October 31, 2024 09:53 2s
feat(MvPolynomial/Degrees): add degreeOf theorems for ^,∑,∏
Add "ready-to-merge" and "delegated" label from comment #62572: Issue comment #18454 (comment) created by riccardobrasca
October 31, 2024 09:39 2s
October 31, 2024 09:39 2s
feat: dividing an element of a euclidean domain by its radical
Add "ready-to-merge" and "delegated" label from comment #62571: Issue comment #18449 (comment) created by mathlib-bors bot
October 31, 2024 09:37 3s
October 31, 2024 09:37 3s