Search results

(WIP) Galois group of <code>x^n - x - 1</code>

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-algebraAlgebra (groups, rings, fields, etc)Algebra (groups, rings, fields, etc)

WIPWork in progressWork in progress

Status: Open (in progress).

leanprover-community/mathlib4number 27053

#27053 In leanprover-community/mathlib4;

· tb65536 opened on Jul 13, 2025

feat: the tensor product of representable functors is representable

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-category-theoryCategory theoryCategory theory

toricPart of the ongoing formalisation of toric varietiesPart of the ongoing formalisation of toric varieties

Status: Open (in progress).

leanprover-community/mathlib4number 27044

#27044 In leanprover-community/mathlib4;

· YaelDillies opened on Jul 12, 2025

feat (Algebra/Order): Hahn embedding theorem part 1

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)

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-algebraAlgebra (groups, rings, fields, etc)Algebra (groups, rings, fields, etc)

WIPWork in progressWork in progress

Status: Draft (not ready).

leanprover-community/mathlib4number 27043

#27043 In leanprover-community/mathlib4;

· wwylele opened on Jul 12, 2025

feat(Analysis/Normed/Group/Quotient): isometric versions of isomorphisms

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

new-contributorThis PR was made by a contributor with at most 5 merged PRs. Welcome to the community!This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!

t-analysisAnalysis (normed *, calculus)Analysis (normed *, calculus)

Status: Open (in progress).

leanprover-community/mathlib4number 27000

#27000 In leanprover-community/mathlib4;

· gasparattila opened on Jul 11, 2025

feat(CategoryTheory): Artinian objects

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-category-theoryCategory theoryCategory theory

Status: Open (in progress).

leanprover-community/mathlib4number 26989

#26989 In leanprover-community/mathlib4;

· joelriou opened on Jul 11, 2025

chore: golf using <code>grw</code>

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)

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

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)

Status: Open (in progress).

leanprover-community/mathlib4number 26981

#26981 In leanprover-community/mathlib4;

· JovanGerb opened on Jul 10, 2025

feat(AlgebraicTopology/ModelCategory): left homotopies

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)

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-category-theoryCategory theoryCategory theory

WIPWork in progressWork in progress

Status: Open (in progress).

leanprover-community/mathlib4number 26967

#26967 In leanprover-community/mathlib4;

· joelriou opened on Jul 10, 2025

feat(AlgebraicTopology/ModelCategory): the lemma by K. S. Brown

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)

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-category-theoryCategory theoryCategory theory

WIPWork in progressWork in progress

Status: Open (in progress).

leanprover-community/mathlib4number 26960

#26960 In leanprover-community/mathlib4;

· joelriou opened on Jul 10, 2025

feat(AlgebraicTopology): path objects in model categories

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)

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-category-theoryCategory theoryCategory theory

WIPWork in progressWork in progress

Status: Open (in progress).

leanprover-community/mathlib4number 26958

#26958 In leanprover-community/mathlib4;

· joelriou opened on Jul 10, 2025

feat(Algebra): unmixed thm of Cohen-Macaulay ring

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)

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-algebraAlgebra (groups, rings, fields, etc)Algebra (groups, rings, fields, etc)

Status: Open (in progress).

leanprover-community/mathlib4number 26957

#26957 In leanprover-community/mathlib4;

· Thmoas-Guan opened on Jul 10, 2025

feat(RingTheory/DividedPowes/SubDPIdeal): complete lattice and quotients

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-algebraAlgebra (groups, rings, fields, etc)Algebra (groups, rings, fields, etc)

Status: Open (in progress).

leanprover-community/mathlib4number 26936

#26936 In leanprover-community/mathlib4;

· mariainesdff opened on Jul 9, 2025

feat(SkewMonoidAlgebra): multiplication and algebraic instances

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-algebraAlgebra (groups, rings, fields, etc)Algebra (groups, rings, fields, etc)

Status: Open (in progress).

leanprover-community/mathlib4number 26933

#26933 In leanprover-community/mathlib4;

· mariainesdff opened on Jul 9, 2025