Search results

feat: add lemmas on <code>spectralRadius</code> along with supporting lemmas

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!

Status: Open (in progress).

leanprover-community/mathlib4number 27993

#27993 In leanprover-community/mathlib4;

· pelicanhere opened on Aug 5, 2025

feat (Rat): add Rat.den_eq_of_add_den_eq_one and its dependent lemmas

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-dataData (lists, quotients, numbers, etc)Data (lists, quotients, numbers, etc)

Status: Open (in progress).

leanprover-community/mathlib4number 27991

#27991 In leanprover-community/mathlib4;

· sinianluoye opened on Aug 5, 2025

chore(Data/Nat/GCD): use <code>Nat.Prime.dvd_or_dvd</code> from #27981 in <code>Nat.Prime.dvd_or_dvd_of_dvd_lcm</code> from #27963 to simplify the proof a bit

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

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!

Status: Open (in progress).

leanprover-community/mathlib4number 27982

#27982 In leanprover-community/mathlib4;

· ShreckYe opened on Aug 5, 2025

feat(Data/Nat/Prime): extract <code>Nat.Prime.dvd_or_dvd</code> from <code>Nat.Prime.dvd_mul</code>

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

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-dataData (lists, quotients, numbers, etc)Data (lists, quotients, numbers, etc)

Status: Open (in progress).

leanprover-community/mathlib4number 27981

#27981 In leanprover-community/mathlib4;

· ShreckYe opened on Aug 5, 2025

feat(Algebra/GCDMonoid): add some theorems related to divisibility and <code>lcm</code> for both <code>GCDMonoid</code> and <code>Nat</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

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

Status: Open (in progress).

leanprover-community/mathlib4number 27963

#27963 In leanprover-community/mathlib4;

· ShreckYe opened on Aug 5, 2025

feat(ProbabilityTheory): Conditional Jensen's Inequality

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)

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-measure-probabilityMeasure theory / Probability theoryMeasure theory / Probability theory

Status: Open (in progress).

leanprover-community/mathlib4number 27953

#27953 In leanprover-community/mathlib4;

· CoolRmal opened on Aug 4, 2025

feat(Order): some Basic lemmas and some SuccOrder <code>biUnion</code> lemmas

carlesonpart of the ongoing formalization of Carleson's theorempart of the ongoing formalization of Carleson's theorem

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-orderOrder theoryOrder theory

Status: Open (in progress).

leanprover-community/mathlib4number 27934

#27934 In leanprover-community/mathlib4;

· JasperMS opened on Aug 4, 2025

feat(Order): add Teichmuller-Tukey lemma

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-orderOrder theoryOrder theory

Status: Open (in progress).

leanprover-community/mathlib4number 27852

#27852 In leanprover-community/mathlib4;

· raja-19 opened on Aug 1, 2025

feat(Geometry/Manifold/ZeroDim): classification of zero dimensional manifolds

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

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-differential-geometryManifolds etcManifolds etc

Status: Open (in progress).

leanprover-community/mathlib4number 27850

#27850 In leanprover-community/mathlib4;

· fyqing opened on Aug 1, 2025

feat(RingTheory/Ideal/Height): sup of ideal heights equals Krull dimension

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-ring-theoryRing theoryRing theory

Status: Open (in progress).

leanprover-community/mathlib4number 27825

#27825 In leanprover-community/mathlib4;

· yonggyuchoimath opened on Aug 1, 2025

feat(CategoryTheory/Sites/Sheaf): functorial version of Sheaf.homEquiv

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)

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

Status: Open (in progress).

leanprover-community/mathlib4number 27821

#27821 In leanprover-community/mathlib4;

· BGuillemet opened on Aug 1, 2025

feat(CategoryTheory/Yoneda): add curried version of Yoneda lemma for heterogeneous universes, and other version of homNatIso

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

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

Status: Open (in progress).

leanprover-community/mathlib4number 27819

#27819 In leanprover-community/mathlib4;

· BGuillemet opened on Aug 1, 2025