Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

Actions: leanprover-community/mathlib3

Actions

Add mathlib4 porting warnings

Actions

Loading...
Loading

Show workflow options

Create status badge

Loading
add_ported_warnings.yml
66 workflow runs
66 workflow runs

Filter by Event

Filter by Status

Filter by Branch

Filter by Actor

old WIP trying to replace fractional_ideal by submodule in class_group: to be ported Add mathlib4 porting warnings #7382: Pull request #19245 synchronize by alreadydone
June 28, 2024 02:36 31s alreadydone:class_group_without_fractional
alreadydone:class_group_without_fractional
June 28, 2024 02:36 31s
old WIP trying to replace fractional_ideal by submodule in class_group: to be ported Add mathlib4 porting warnings #7381: Pull request #19245 reopened by alreadydone
June 28, 2024 02:36 29s alreadydone:class_group_without_fractional
alreadydone:class_group_without_fractional
June 28, 2024 02:36 29s
old WIP trying to replace fractional_ideal by submodule in class_group: to be ported Add mathlib4 porting warnings #7380: Pull request #19245 opened by alreadydone
June 28, 2024 00:09 31s alreadydone:class_group_without_fractional
alreadydone:class_group_without_fractional
June 28, 2024 00:09 31s
feat(ring_theory/integral_domain): generalize card_fiber_eq_of_mem_range Add mathlib4 porting warnings #7379: Pull request #17653 synchronize by urkud
February 11, 2024 05:58 27s YK-card-fiber-eq
YK-card-fiber-eq
February 11, 2024 05:58 27s
refactor: Remove the K argument from exp Add mathlib4 porting warnings #7378: Pull request #19244 synchronize by eric-wieser
November 12, 2023 12:55 32s eric-wieser/exp-rat
eric-wieser/exp-rat
November 12, 2023 12:55 32s
refactor: Remove the K argument from exp Add mathlib4 porting warnings #7377: Pull request #19244 opened by eric-wieser
November 12, 2023 12:46 33s eric-wieser/exp-rat
eric-wieser/exp-rat
November 12, 2023 12:46 33s
feat(combinatorics/additive/kneser): Kneser's addition theorem Add mathlib4 porting warnings #7376: Pull request #19000 synchronize by YaelDillies
October 31, 2023 15:30 42s kneser
kneser
October 31, 2023 15:30 42s
feat(combinatorics/additive/erdos_ginzburg_ziv): The Erdős–Ginzburg–Ziv theorem Add mathlib4 porting warnings #7375: Pull request #18063 synchronize by YaelDillies
October 30, 2023 22:51 32s erdos_ginzburg_ziv
erdos_ginzburg_ziv
October 30, 2023 22:51 32s
feat(combinatorics/simple_graph): Locally linear graphs Add mathlib4 porting warnings #7374: Pull request #19201 synchronize by YaelDillies
October 23, 2023 07:19 35s locally_linear_graph
locally_linear_graph
October 23, 2023 07:19 35s
feat(combinatorics/simple_graph): Locally linear graphs Add mathlib4 porting warnings #7373: Pull request #19201 synchronize by YaelDillies
October 23, 2023 07:13 37s locally_linear_graph
locally_linear_graph
October 23, 2023 07:13 37s
feat(tactic/polyrith): solve more problems by testing for membership in the radical Add mathlib4 porting warnings #7372: Pull request #15425 synchronize by robertylewis
October 18, 2023 01:48 38s polyrith-radical
polyrith-radical
October 18, 2023 01:48 38s
[Merged by Bors] - feat(measure_theory/order/upper_lower): Order-connected sets in ℝⁿ are measurable Add mathlib4 porting warnings #7371: Pull request #16976 synchronize by YaelDillies
October 16, 2023 09:23 43s ord_connected_measurable
ord_connected_measurable
October 16, 2023 09:23 43s
feat(algebra/incidence): Incidence algebras Add mathlib4 porting warnings #7370: Pull request #11656 synchronize by eric-wieser
October 11, 2023 13:07 2m 59s incidence_algebra
incidence_algebra
October 11, 2023 13:07 2m 59s
[Merged by Bors] - doc: Add a warning mentioning Lean 4 to the readme Add mathlib4 porting warnings #7369: Pull request #19243 synchronize by eric-wieser
October 10, 2023 21:53 42s eric-wieser/readme-admonition
eric-wieser/readme-admonition
October 10, 2023 21:53 42s
[Merged by Bors] - doc: Add a warning mentioning Lean 4 to the readme Add mathlib4 porting warnings #7368: Pull request #19243 opened by eric-wieser
October 10, 2023 21:46 35s eric-wieser/readme-admonition
eric-wieser/readme-admonition
October 10, 2023 21:46 35s
chore(LinearAlgebra/DirectSum/TensorProduct): missing lemma Add mathlib4 porting warnings #7367: Pull request #19242 opened by eric-wieser
September 27, 2023 10:14 39s eric-wieser/directSum_symm_lof_tmul
eric-wieser/directSum_symm_lof_tmul
September 27, 2023 10:14 39s
[Merged by Bors] - feat(measure_theory/order/upper_lower): Order-connected sets in ℝⁿ are measurable Add mathlib4 porting warnings #7366: Pull request #16976 synchronize by YaelDillies
September 19, 2023 10:08 41s ord_connected_measurable
ord_connected_measurable
September 19, 2023 10:08 41s
[Merged by Bors] - feat(measure_theory/order/upper_lower): Order-connected sets in ℝⁿ are measurable Add mathlib4 porting warnings #7365: Pull request #16976 synchronize by YaelDillies
September 19, 2023 10:07 37s ord_connected_measurable
ord_connected_measurable
September 19, 2023 10:07 37s
[Merged by Bors] - feat(measure_theory/order/upper_lower): Order-connected sets in ℝⁿ are measurable Add mathlib4 porting warnings #7364: Pull request #16976 synchronize by YaelDillies
September 19, 2023 10:05 36s ord_connected_measurable
ord_connected_measurable
September 19, 2023 10:05 36s
[Merged by Bors] - feat(measure_theory/order/upper_lower): Order-connected sets in ℝⁿ are measurable Add mathlib4 porting warnings #7363: Pull request #16976 synchronize by YaelDillies
September 19, 2023 09:43 43s ord_connected_measurable
ord_connected_measurable
September 19, 2023 09:43 43s
[Merged by Bors] - feat(topology/algebra/order/liminf_limsup): Eventual boundedness of neighborhoods Add mathlib4 porting warnings #7362: Pull request #18629 synchronize by YaelDillies
September 18, 2023 15:31 36s bounded_le_nhds_class
bounded_le_nhds_class
September 18, 2023 15:31 36s
feat(combinatorics/set_family/kruskal_katona): The Kruskal-Katona theorem Add mathlib4 porting warnings #7361: Pull request #2770 synchronize by YaelDillies
September 17, 2023 20:14 36s combinatorics
combinatorics
September 17, 2023 20:14 36s
feat(combinatorics/set_family/ahlswede_zhang): Ahlswede-Zhang identity, part II Add mathlib4 porting warnings #7360: Pull request #18618 synchronize by YaelDillies
September 14, 2023 19:56 33s ahlswede_zhang
ahlswede_zhang
September 14, 2023 19:56 33s
[Merged by Bors] - feat(combinatorics/set_family/ahlswede_zhang): Ahlswede-Zhang identity, part I Add mathlib4 porting warnings #7359: Pull request #18612 synchronize by YaelDillies
September 12, 2023 13:11 46s truncated_sup
truncated_sup
September 12, 2023 13:11 46s
[Merged by Bors] - feat(probability/independence): Independence of singletons Add mathlib4 porting warnings #7358: Pull request #18506 synchronize by YaelDillies
September 12, 2023 09:00 35s generate_from_singleton
generate_from_singleton
September 12, 2023 09:00 35s