Search results

feat: simple lemmas on circle integrability

easy< 20s of review time. See the lifecycle page for guidelines.< 20s of review time. See the lifecycle page for guidelines.

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

t-measure-probabilityMeasure theory / Probability theoryMeasure theory / Probability theory

Status: Open (in progress).

leanprover-community/mathlib4number 26618

#26618 In leanprover-community/mathlib4;

· kebekus opened on Jul 2, 2025

chore: fix minor docstring mistake LHS → RHS

easy< 20s of review time. See the lifecycle page for guidelines.< 20s of review time. See the lifecycle page for guidelines.

t-orderOrder theoryOrder theory

Status: Open (in progress).

leanprover-community/mathlib4number 26610

#26610 In leanprover-community/mathlib4;

· vihdzp opened on Jul 2, 2025

chore: <code>GRewrite</code> typo

easy< 20s of review time. See the lifecycle page for guidelines.< 20s of review time. See the lifecycle page for guidelines.

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

Status: Open (in progress).

leanprover-community/mathlib4number 26604

#26604 In leanprover-community/mathlib4;

· DavidLedvinka opened on Jul 2, 2025

chore: declare <code>T₀ ∧ R₀ → T₁</code> as an instance

easy< 20s of review time. See the lifecycle page for guidelines.< 20s of review time. See the lifecycle page for guidelines.

t-topologyTopological spaces, uniform spaces, metric spaces, filtersTopological spaces, uniform spaces, metric spaces, filters

Status: Open (in progress).

leanprover-community/mathlib4number 26550

#26550 In leanprover-community/mathlib4;

· Komyyy opened on Jun 30, 2025

feat(Algebra/Order/Archimedean): (Mul)Archimedean.comap

easy< 20s of review time. See the lifecycle page for guidelines.< 20s of review time. See the lifecycle page for guidelines.

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

t-orderOrder theoryOrder theory

Status: Open (in progress).

leanprover-community/mathlib4number 26548

#26548 In leanprover-community/mathlib4;

· pechersky opened on Jun 30, 2025

feat(Geometry/Euclidean/Projection): projection onto a 0-simplex

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)

easy< 20s of review time. See the lifecycle page for guidelines.< 20s of review time. See the lifecycle page for guidelines.

t-euclidean-geometryAffine and axiomatic geometryAffine and axiomatic geometry

Status: Open (in progress).

leanprover-community/mathlib4number 26529

#26529 In leanprover-community/mathlib4;

· jsm28 opened on Jun 29, 2025

feat(LinearAlgebra/AffineSpace/Independent): <code>faceOpposite</code> point in 1-simplex

easy< 20s of review time. See the lifecycle page for guidelines.< 20s of review time. See the lifecycle page for guidelines.

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

Status: Open (in progress).

leanprover-community/mathlib4number 26527

#26527 In leanprover-community/mathlib4;

· jsm28 opened on Jun 29, 2025

feat(Order): complementary under sublattice

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)

easy< 20s of review time. See the lifecycle page for guidelines.< 20s of review time. See the lifecycle page for guidelines.

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

Status: Open (in progress).

leanprover-community/mathlib4number 26513

#26513 In leanprover-community/mathlib4;

· wwylele opened on Jun 29, 2025

feat(RingTheory/Valuation/Integers): nontrivial_iff

easy< 20s of review time. See the lifecycle page for guidelines.< 20s of review time. See the lifecycle page for guidelines.

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

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

t-number-theoryNumber theory (also use t-algebra or t-analysis to specialize)Number theory (also use t-algebra or t-analysis to specialize)

Status: Open (in progress).

leanprover-community/mathlib4number 26512

#26512 In leanprover-community/mathlib4;

· pechersky opened on Jun 29, 2025

add some lemmas about <code>Nat.gcd</code>

easy< 20s of review time. See the lifecycle page for guidelines.< 20s of review time. See the lifecycle page for guidelines.

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

Status: Open (in progress).

leanprover-community/mathlib4number 26488

#26488 In leanprover-community/mathlib4;

· yuanyi-350 opened on Jun 28, 2025

feat(Order): Add curried versions of <code>biSup_prod</code> and <code>biInf_prod</code>

easy< 20s of review time. See the lifecycle page for guidelines.< 20s of review time. See the lifecycle page for guidelines.

t-orderOrder theoryOrder theory

Status: Open (in progress).

leanprover-community/mathlib4number 26486

#26486 In leanprover-community/mathlib4;

· DavidLedvinka opened on Jun 28, 2025

doc: remove <code>PartENat.card</code> in the module doc

documentationImprovements or additions to documentationImprovements or additions to documentation

easy< 20s of review time. See the lifecycle page for guidelines.< 20s of review time. See the lifecycle page for guidelines.

maintainer-merge

t-set-theorySet theorySet theory

Status: Open (in progress).

leanprover-community/mathlib4number 26426

#26426 In leanprover-community/mathlib4;

· Komyyy opened on Jun 26, 2025