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

Actions

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

Actions

Loading...
Loading

47,925 workflow runs

perf: hard-code typeclass inference in linarith Add "ready-to-merge" and "delegated" label from comment #63510: Issue comment #18714 (comment) created by grunweg

November 7, 2024 12:53

refactor(RingTheory/Ideal/Pointwise): Make Ideal.IsPrime.smul into an instance Add "ready-to-merge" and "delegated" label from comment #63509: Issue comment #18241 (comment) created by riccardobrasca

November 7, 2024 12:43

[Merged by Bors] - feat(NumberField/CanonicalEmbedding): put an euclidean space structure on the mixed space Add "ready-to-merge" and "delegated" label from comment #63508: Issue comment #18245 (comment) created by mathlib-bors bot

November 7, 2024 12:25

[Merged by Bors] - feat: define restrictions of perfect pairings Add "ready-to-merge" and "delegated" label from comment #63507: Issue comment #18559 (comment) created by mathlib-bors bot

November 7, 2024 12:25

chore: unify binary inf and min Add "ready-to-merge" and "delegated" label from comment #63506: Issue comment #18707 (comment) created by sven-manthe

November 7, 2024 12:21

[Merged by Bors] - chore: deprecate Nat.le_div_iff_mul_le' and Nat.div_lt_iff_lt_mul' Add "ready-to-merge" and "delegated" label from comment #63505: Issue comment #18721 (comment) created by mathlib-bors bot

November 7, 2024 11:59

feat: Mason-Stothers theorem (polynomial ABC) Add "ready-to-merge" and "delegated" label from comment #63504: Issue comment #15706 (comment) created by jcpaik

November 7, 2024 11:53

feat(LinearAlgebra): generators of pi tensor products Add "ready-to-merge" and "delegated" label from comment #63503: Issue comment #18725 (comment) created by mathlib4-dependent-issues-bot

November 7, 2024 11:46

[Merged by Bors] - feat(NumberField/CanonicalEmbedding): put an euclidean space structure on the mixed space Add "ready-to-merge" and "delegated" label from comment #63502: Issue comment #18245 (comment) created by xroblot

November 7, 2024 11:46

13s

November 7, 2024 11:46

13s

refactor(RingTheory/Ideal/Pointwise): Make Ideal.IsPrime.smul into an instance Add "ready-to-merge" and "delegated" label from comment #63501: Issue comment #18241 (comment) created by leanprover-bot

November 7, 2024 11:28

[Merged by Bors] - chore: deprecate Nat.le_div_iff_mul_le' and Nat.div_lt_iff_lt_mul' Add "ready-to-merge" and "delegated" label from comment #63500: Issue comment #18721 (comment) created by riccardobrasca

November 7, 2024 11:20

18s

November 7, 2024 11:20

18s

refactor(RingTheory/Ideal/Pointwise): Make Ideal.IsPrime.smul into an instance Add "ready-to-merge" and "delegated" label from comment #63499: Issue comment #18241 (comment) created by riccardobrasca

November 7, 2024 11:02

feat: Mason-Stothers theorem (polynomial ABC) Add "ready-to-merge" and "delegated" label from comment #63498: Issue comment #15706 (comment) created by riccardobrasca

November 7, 2024 11:01

feat(Data/Fin/Parity): add lemmas about parity of Fin numbers Add "ready-to-merge" and "delegated" label from comment #63497: Issue comment #8960 (comment) created by Command-Master

November 7, 2024 10:25

chore(Data/Finset): split Basic.lean into many smaller files Add "ready-to-merge" and "delegated" label from comment #63496: Issue comment #18610 (comment) created by Vierkantor

November 7, 2024 10:10

feat: Abstract Frobenius elements Add "ready-to-merge" and "delegated" label from comment #63495: Issue comment #14155 (comment) created by kbuzzard

November 7, 2024 09:39

[Merged by Bors] - feat(RingTheory/Localization/FractionRing): fieldEquivOfAlgEquivHom is injective Add "ready-to-merge" and "delegated" label from comment #63494: Issue comment #18703 (comment) created by mathlib-bors bot

November 7, 2024 09:25

[Merged by Bors] - feat(NumberField/CanonicalEmbedding): put an euclidean space structure on the mixed space Add "ready-to-merge" and "delegated" label from comment #63493: Issue comment #18245 (comment) created by mathlib-bors bot

November 7, 2024 09:22

[Merged by Bors] - feat(RingTheory/Localization/FractionRing): fieldEquivOfAlgEquivHom is injective Add "ready-to-merge" and "delegated" label from comment #63492: Issue comment #18703 (comment) created by riccardobrasca

November 7, 2024 09:06

15s

November 7, 2024 09:06

15s

[Merged by Bors] - feat: duality results for cyclic groups Add "ready-to-merge" and "delegated" label from comment #63491: Issue comment #18687 (comment) created by mathlib-bors bot

November 7, 2024 09:03

[Merged by Bors] - feat: duality results for cyclic groups Add "ready-to-merge" and "delegated" label from comment #63490: Issue comment #18687 (comment) created by kim-em

November 7, 2024 08:50

15s

November 7, 2024 08:50

15s

feat: induction principle for ENNReal-valued measurable functions from a sigma-finite space Add "ready-to-merge" and "delegated" label from comment #63489: Issue comment #17835 (comment) created by mathlib-bors bot

November 7, 2024 08:42

[Merged by Bors] - fix: make sure that a MeasurableSpace instance uses Discreteness Add "ready-to-merge" and "delegated" label from comment #63488: Issue comment #18494 (comment) created by mathlib-bors bot

November 7, 2024 08:30

feat: induction principle for ENNReal-valued measurable functions from a sigma-finite space Add "ready-to-merge" and "delegated" label from comment #63487: Issue comment #17835 (comment) created by YaelDillies

November 7, 2024 08:29

10s

November 7, 2024 08:29

10s

[Merged by Bors] - chore: replace unfold_let with unfold Add "ready-to-merge" and "delegated" label from comment #63486: Issue comment #18645 (comment) created by mathlib-bors bot

November 7, 2024 08:22

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Actions

Workflows

Management