Search results

refactor: deprecate <code>SemilinearMapClass</code>

awaiting-bench

blocked-by-other-PRThis PR depends on another PR (this label is automatically managed by a bot)This PR depends on another PR (this label is automatically managed by a bot)

merge-conflictThe PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot)The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot)

t-algebraAlgebra (groups, rings, fields, etc)Algebra (groups, rings, fields, etc)

WIPWork in progressWork in progress

Status: Draft (not ready).

leanprover-community/mathlib4number 18805

#18805 In leanprover-community/mathlib4;

· astrainfinita opened on Nov 10, 2024

perf: lower the priority of <code>SemilinearMapClass.toAddHomClass</code>

awaiting-bench

merge-conflictThe PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot)The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot)

slow-typeclass-synthesis

t-algebraAlgebra (groups, rings, fields, etc)Algebra (groups, rings, fields, etc)

Status: Draft (not ready).

leanprover-community/mathlib4number 18719

#18719 In leanprover-community/mathlib4;

· astrainfinita opened on Nov 7, 2024

perf: change the priority of <code>*.toSemiring</code> instances

awaiting-bench

blocked-by-other-PRThis PR depends on another PR (this label is automatically managed by a bot)This PR depends on another PR (this label is automatically managed by a bot)

slow-typeclass-synthesis

t-algebraAlgebra (groups, rings, fields, etc)Algebra (groups, rings, fields, etc)

WIPWork in progressWork in progress

Status: Open (in progress).

leanprover-community/mathlib4number 18706

#18706 In leanprover-community/mathlib4;

· astrainfinita opened on Nov 6, 2024

perf: change the priority of <code>*.toRing</code> instances

awaiting-bench

blocked-by-other-PRThis PR depends on another PR (this label is automatically managed by a bot)This PR depends on another PR (this label is automatically managed by a bot)

slow-typeclass-synthesis

t-algebraAlgebra (groups, rings, fields, etc)Algebra (groups, rings, fields, etc)

Status: Open (in progress).

leanprover-community/mathlib4number 18641

#18641 In leanprover-community/mathlib4;

· astrainfinita opened on Nov 5, 2024

perf: lower the priority of <code>Comm*.to*</code> instances

awaiting-bench

blocked-by-other-PRThis PR depends on another PR (this label is automatically managed by a bot)This PR depends on another PR (this label is automatically managed by a bot)

slow-typeclass-synthesis

t-algebraAlgebra (groups, rings, fields, etc)Algebra (groups, rings, fields, etc)

Status: Open (in progress).

leanprover-community/mathlib4number 18472

#18472 In leanprover-community/mathlib4;

· astrainfinita opened on Oct 30, 2024

perf: lower the priority of <code>toMul</code> and <code>toAdd</code> instances

awaiting-bench

blocked-by-other-PRThis PR depends on another PR (this label is automatically managed by a bot)This PR depends on another PR (this label is automatically managed by a bot)

slow-typeclass-synthesis

t-algebraAlgebra (groups, rings, fields, etc)Algebra (groups, rings, fields, etc)

Status: Open (in progress).

leanprover-community/mathlib4number 18464

#18464 In leanprover-community/mathlib4;

· astrainfinita opened on Oct 30, 2024

perf: make <code>Mul.toSMul</code> higher priority

awaiting-bench

merge-conflictThe PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot)The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot)

t-algebraAlgebra (groups, rings, fields, etc)Algebra (groups, rings, fields, etc)

Status: Draft (not ready).

leanprover-community/mathlib4number 18294

#18294 In leanprover-community/mathlib4;

· astrainfinita opened on Oct 27, 2024

perf: do not search algebraic hierarchies when using <code>map_*</code> lemmas

awaiting-bench

merge-conflictThe PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot)The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot)

t-algebraAlgebra (groups, rings, fields, etc)Algebra (groups, rings, fields, etc)

WIPWork in progressWork in progress

Status: Open (in progress).

leanprover-community/mathlib4number 17513

#17513 In leanprover-community/mathlib4;

· astrainfinita opened on Oct 7, 2024

feat: add <code>Decidable</code>, <code>Fintype</code>, <code>Encodable</code> linters

awaiting-authorA reviewer has asked the author a question or requested changes.A reviewer has asked the author a question or requested changes.

awaiting-bench

large-importAutomatically added label for PRs with a significant increase in transitive importsAutomatically added label for PRs with a significant increase in transitive imports

t-linterLinterLinter

t-metaTactics, attributes or user commandsTactics, attributes or user commands

Status: Open (in progress).

leanprover-community/mathlib4number 10235

#10235 In leanprover-community/mathlib4;

· urkud opened on Feb 4, 2024