SnirBroshi/mathlib4

[`SimpleGraph/Hamiltonian`] Graphs with Hamiltonian/Eulerian walks are connected about 9 hours ago

help wanted graph-theory

SnirBroshi/mathlib4

1

The math library of Lean 4

[`SimpleGraph/Trails`] existence of an Eulerian walk about 9 hours ago

help wanted graph-theory

SnirBroshi/mathlib4

1

The math library of Lean 4

[`SimpleGraph/Eulerian`] Explicit construction of an Eulerian circuit for `completeGraph (Fin (2 * n + 1))` about 9 hours ago

help wanted graph-theory

SnirBroshi/mathlib4

1

The math library of Lean 4

[`Logic/Relation`] add missing theorems and instances 1 day ago

help wanted

SnirBroshi/mathlib4

1

The math library of Lean 4

[`SimpleGraph/Walk`] Properties and operations 3 days ago

help wanted graph-theory

SnirBroshi/mathlib4

1

The math library of Lean 4

Bundle matrix morphisms 5 days ago

help wanted algebra

SnirBroshi/mathlib4

1

The math library of Lean 4

[`SimpleGraph`] Properties and operations 6 days ago

help wanted graph-theory

SnirBroshi/mathlib4

1

The math library of Lean 4

Skew-symmetric / skew-hermitian matrices 6 days ago

help wanted

SnirBroshi/mathlib4

1

The math library of Lean 4

[`Combinatorics/Enumerative/Stirling`] relate both kinds of Stirling numbers to counting problems 8 days ago

help wanted

SnirBroshi/mathlib4

1

The math library of Lean 4

[`SimpleGraph`] `Sigma` operation 13 days ago

help wanted graph-theory

SnirBroshi/mathlib4

1

The math library of Lean 4

[`SimpleGraph/Prod`] Coloring API for the tensor product 15 days ago

help wanted graph-theory

SnirBroshi/mathlib4

1

The math library of Lean 4

`Real.exp` sequence bounds 29 days ago

help wanted analysis

SnirBroshi/mathlib4

1

The math library of Lean 4

[`Analysis/MeanInequalities`] Fill in API about 1 month ago

help wanted analysis

SnirBroshi/mathlib4

1

The math library of Lean 4

[`SimpleGraph/LapMatrix`] Spectra of known graphs about 1 month ago

help wanted graph-theory

SnirBroshi/mathlib4

1

The math library of Lean 4

Complex analysis about 2 months ago

help wanted analysis

SnirBroshi/mathlib4

1

The math library of Lean 4

[`RingTheory/RootsOfUnity`] The sum of all roots of unity is 0 and other trivial stuff about 2 months ago

help wanted analysis

SnirBroshi/mathlib4

1

The math library of Lean 4

`Subtype.restrict` / `Set.restrict` / `Finset.restrict` about 2 months ago

help wanted

SnirBroshi/mathlib4

1

The math library of Lean 4

Properties of `Matrix.rank` / `Matrix.cRank` about 2 months ago

help wanted algebra

SnirBroshi/mathlib4

1

The math library of Lean 4

Summing `ENat` 2 months ago

help wanted

SnirBroshi/mathlib4

1

The math library of Lean 4

[`SimpleGraph`] Menger's theorems 3 months ago

help wanted graph-theory

SnirBroshi/mathlib4

1

The math library of Lean 4

[`SimpleGraph/Paths`] Any two longest paths in a preconnected graph intersect 3 months ago

help wanted graph-theory

SnirBroshi/mathlib4

1

The math library of Lean 4

The Rado graph 3 months ago

help wanted graph-theory

SnirBroshi/mathlib4

1

The math library of Lean 4

[`RingTheory/Algebraic`] `Transcendental`/`IsAlgebraic` over fraction rings 3 months ago

help wanted algebra

SnirBroshi/mathlib4

1

The math library of Lean 4

Integral representation of the Zeta function 3 months ago

help wanted analysis

SnirBroshi/mathlib4

1

The math library of Lean 4

[`NumberTheory/Real/Irrational`] `Decidable <| Irrational <| q ^ p` for `q p : ℚ` 4 months ago

help wanted number-theory

SnirBroshi/mathlib4

1

The math library of Lean 4

[`Counterexamples`] Lakes of Wada 4 months ago

help wanted topology

SnirBroshi/mathlib4

1

The math library of Lean 4

[`Analysis/SpecialFunctions/Gamma/Beta`] `Γ(s - 1) = Γ(s + 1)` iff 4 months ago

help wanted analysis

SnirBroshi/mathlib4

1

The math library of Lean 4

[`NumberTheory/Transcendental/Liouville/LiouvilleNumber`] Liouville numbers using digits other than 1 4 months ago

help wanted number-theory

SnirBroshi/mathlib4

1

The math library of Lean 4

[`SimpleGraph/Paths`] A walk is a path iff its subgraph is acyclic 4 months ago

help wanted graph-theory

SnirBroshi/mathlib4

1

The math library of Lean 4

[`SimpleGraph/Connectivity`] Connectivity vs adding edges 4 months ago

help wanted graph-theory

SnirBroshi/mathlib4

1

The math library of Lean 4

[`NumberTheory/SumThreeSquares`] Legendre's three-square theorem 4 months ago

help wanted number-theory

SnirBroshi/mathlib4

1

The math library of Lean 4

[`Algebra/LinearRecurrence`] Pisano periods 4 months ago

help wanted

SnirBroshi/mathlib4

1

The math library of Lean 4

Circumference of a circle 4 months ago

help wanted

SnirBroshi/mathlib4

1

The math library of Lean 4

[`Analysis/Normed/Algebra/MatrixExponential`] det / trace / eigenvalues 4 months ago

help wanted

SnirBroshi/mathlib4

1

The math library of Lean 4

Van der Waerden and Schur numbers 4 months ago

help wanted

SnirBroshi/mathlib4

1

The math library of Lean 4

[`SimpleGraph/Acyclic`] Add `IsTrail` versions of acyclic theorems 4 months ago

help wanted graph-theory

SnirBroshi/mathlib4

1

The math library of Lean 4

[`FieldTheory/Perfect`] Prove equivalences 4 months ago

help wanted algebra

SnirBroshi/mathlib4

1

The math library of Lean 4

[`SimpleGraph/Prod`] Define the tensor product 4 months ago

help wanted graph-theory

SnirBroshi/mathlib4

1

The math library of Lean 4

[`SimpleGraph`] Hadwiger-Nelson problem 4 months ago

help wanted graph-theory

SnirBroshi/mathlib4

1

The math library of Lean 4

[`SimpleGraph`] Mycielskian 4 months ago

help wanted graph-theory

SnirBroshi/mathlib4

1

The math library of Lean 4

[`SimpleGraph`] Dominating sets and domination number 4 months ago

help wanted graph-theory

SnirBroshi/mathlib4

1

The math library of Lean 4

[`SimpleGraph`] Perfect graphs 4 months ago

help wanted graph-theory

SnirBroshi/mathlib4

1

The math library of Lean 4

[`SimpleGraph/Circulant`] `(cycleGraph <| 2 * k + 1)ᶜ.cliqueNum = k` 4 months ago

help wanted graph-theory

SnirBroshi/mathlib4

1

The math library of Lean 4

[`SimpleGraph/ConcreteColorings`] `(cycleGraph <| 2 * k + 1)ᶜ.chromaticNumber = k + 1` 4 months ago

help wanted graph-theory

SnirBroshi/mathlib4

1

The math library of Lean 4

[`SimpleGraph`] Paths and incidence sets / degrees 4 months ago

help wanted graph-theory

SnirBroshi/mathlib4

1

The math library of Lean 4

[`NumberTheory/Complex`] `re`/`im`/`star` are algebraic 4 months ago

help wanted

SnirBroshi/mathlib4

1

The math library of Lean 4

Hermite's identity 4 months ago

help wanted

SnirBroshi/mathlib4

1

The math library of Lean 4

[`Analysis/Arctan`] `StrictMono (x - Real.arctan x)` 4 months ago

help wanted analysis

SnirBroshi/mathlib4

1

The math library of Lean 4

[`SimpleGraph`] Longest paths in acyclic graphs are between leaves 4 months ago

help wanted graph-theory

SnirBroshi/mathlib4

1

The math library of Lean 4

[`SimpleGraph/Walks/Operations`] `take` and `drop` 4 months ago

help wanted graph-theory

SnirBroshi/mathlib4

1

The math library of Lean 4

[`SimpleGraph`] Existence of paths of length `edist` / `eccent` / `ediam` / `radius` 4 months ago

help wanted graph-theory

SnirBroshi/mathlib4

1

The math library of Lean 4

[`SimpleGraph`] Longest path iff length equals diameter / eccentricity 4 months ago

help wanted graph-theory

SnirBroshi/mathlib4

1

The math library of Lean 4

[`SimpleGraph`] Shortest walks are paths 4 months ago

help wanted graph-theory

SnirBroshi/mathlib4

1

The math library of Lean 4

[`SimpleGraph`] Calculating the diameter 4 months ago

help wanted graph-theory

SnirBroshi/mathlib4

1

The math library of Lean 4

[`SimpleGraph/Connectivity/Connected`] Change `connected_delete_edge_of_not_isBridge` to only require `Preconnected` 4 months ago

help wanted graph-theory

SnirBroshi/mathlib4

1

The math library of Lean 4

[`SimpleGraph/Clique`] Expand independent sets API 4 months ago

help wanted graph-theory

SnirBroshi/mathlib4

1

The math library of Lean 4

[`SimpleGraph/Connectivity/WalkDecomp`] `reverse` / `takeUntil` / `dropUntil` 5 months ago

help wanted graph-theory

SnirBroshi/mathlib4

1

The math library of Lean 4

Deprecate `Order.Preimage` and `InvImage` in favor of `Function.onFun` 5 months ago

help wanted

SnirBroshi/mathlib4

1

The math library of Lean 4

[Topology] Rename `ZerothHomotopy` to `PathConnectedComponent` 5 months ago

help wanted topology

SnirBroshi/mathlib4

1

The math library of Lean 4

Open Issues Need Help