Commits

Branch selector

 master

User selector

IvanRenison

All time

Commit History

Commits on Mar 5, 2026

• feat(Data/List): add theorem `length_eq_two'` (#35775)

  IvanRenison

  committed
  8e1dd63

  Copy full SHA for 8e1dd63

Commits on Feb 26, 2026

• feat(Combinatorics/SimpleGraph/Diam): drop `Finite α` from `ediam_le_two_mul_radius` (#33764)

  IvanRenison

  committed
  2fff144

  Copy full SHA for 2fff144

Commits on Jan 27, 2026

• feat(Combinatorics/SimpleGraph/Connectivity): add lemma `not_reachable_of_{left, right}_degree_zero` (#34492)

  IvanRenison

  committed
  b805661

  Copy full SHA for b805661

Commits on Jan 18, 2026

• feat(Combinatorics/SimpleGraph/Diam): add lemma `eccent_eq_one_iff` (#34085)

  IvanRenison

  committed
  cf98ec8

  Copy full SHA for cf98ec8

Commits on Nov 28, 2025

• feat(Combinatorics/SimpleGraph): Probe that all trees are bipartite (#32185)

  Show description for 143c343
  

  IvanRenison

  and

  guelmi94

  committed
  143c343

  Copy full SHA for 143c343

Commits on Nov 27, 2025

• feat(Combinatorics/SimpleGraph): add lemma `IsTree.dist_ne_of_adj` and necessary lemmas (#30069)

  Show description for 4e83287
  

  IvanRenison

  and

  pre-commit-ci-lite[bot]

  committed
  4e83287

  Copy full SHA for 4e83287

Commits on Sep 28, 2025

• feat(Combinatorics/SimpleGraph/Paths): add lemma `SimpleGraph.Walk.IsPath.mem_support_iff_exists_append` (#27461)

  Show description for b8f1ced
  IvanRenison

  committed
  b8f1ced

  Copy full SHA for b8f1ced

• feat(Combinatorics/SimpleGraph): add theorem `SimpleGraph.Connected.diff_dist_adj` (#27468)

  Show description for 652dbc7
  IvanRenison

  committed
  652dbc7

  Copy full SHA for 652dbc7

Commits on Sep 3, 2025

• feat(Combinatorics/SimpleGraph/Walk): add theorems about the support of `Walk.cons` and `Walk.concat` (#27460)

  Show description for 314177a
  IvanRenison

  committed
  314177a

  Copy full SHA for 314177a

Commits on Aug 24, 2025

• feat(Combinatorics/SimpleGraph/Paths): add lemma `SimpleGraph.Walk.IsPath.ne_of_mem_support_of_append` (#27464)

  Show description for eb13ab8
  IvanRenison

  committed
  eb13ab8

  Copy full SHA for eb13ab8

Commits on Aug 15, 2025

• feat(Combinatorics/SimpleGraph/Paths): add theorem `SimpleGraph.Walk.IsPath.concat` (#27582)

  Show description for 3fe589e
  IvanRenison

  committed
  3fe589e

  Copy full SHA for 3fe589e

Commits on Jul 28, 2025

• feat(Analysis/InnerProductSpace/Positive.): add theorem `LinearMap.IsPositive.of_isStarProjection` (#27246)

  Show description for 554c34a
  IvanRenison

  committed
  554c34a

  Copy full SHA for 554c34a

Commits on Jul 26, 2025

• feat(Data/List): add theorem `List.nodup_concat` (#27459)

  Show description for 7cd224f
  IvanRenison

  committed
  7cd224f

  Copy full SHA for 7cd224f

Commits on Jul 19, 2025

• feat(Analysis/InnerProductSpace/Positive): add theorem `LinearMap.IsPositive.adjoint_eq` (#27195)

  IvanRenison

  committed
  58a7c6f

  Copy full SHA for 58a7c6f

Commits on Jun 30, 2025

• feat(Analysis/InnerProductSpace/Positive): add theorem `LinearMap.IsPositive.smul_of_zero_le` (#26425)

  IvanRenison

  committed
  46f25b0

  Copy full SHA for 46f25b0

Commits on Jun 20, 2025

• feat(Analysis/InnerProductSpace/Trace): prove that the trace of a symmetric linear map is equal to the sum of its eigenvalues (#26026)

  IvanRenison

  committed
  3a374b3

  Copy full SHA for 3a374b3

Commits on Jun 10, 2025

• feat(Analysis/InnerProductSpace/Projection): add lemma `Submodule.le_iff_orthogonal_le_orthogonal` and similars (#25240)

  IvanRenison

  committed
  5bc4d64

  Copy full SHA for 5bc4d64

Commits on Jun 9, 2025

• feat(Analysis/InnerProductSpace/Positive): add theorem `IsPositive.nonneg_eigenvalues` (#25493)

  IvanRenison

  committed
  3e523a1

  Copy full SHA for 3e523a1

Commits on Jun 8, 2025

• feat(Combinatorics/SimpleGraph): introduce `ConnectedComponent.toSimpleGraph` (#22085)

  IvanRenison

  committed
  d1c754c

  Copy full SHA for d1c754c

Commits on Jun 4, 2025

• feat: define `IsPositive` and Löwner order for `LinearMap` (#24471)

  Show description for 6455ba8
  IvanRenison

  committed
  6455ba8

  Copy full SHA for 6455ba8

Commits on May 31, 2025

• feat(Analysis/InnerProductSpace): add direct formula for trace of linear map with respect to an orthonormal basis (#25233)

  IvanRenison

  committed
  644a230

  Copy full SHA for 644a230

• feat(Analysis/InnerProductSpace/Projection): add `Submodule.re_inner_orthogonalProjection_nonneg` (#24659)

  IvanRenison

  committed
  dd00819

  Copy full SHA for dd00819

Commits on May 29, 2025

• feat(Analysis/RCLike): add theorem `RCLike.zero_im` and fix name of `RCLike.zero_re` (#25077)

  Show description for 520939f
  IvanRenison

  committed
  520939f

  Copy full SHA for 520939f

Commits on May 4, 2025

• feat(Combinatorics/SimpleGraph): Add `SimpleGraph.Preconnected.support_eq_univ` (#22050)

  Show description for 9c5455a
  IvanRenison

  committed
  9c5455a

  Copy full SHA for 9c5455a

Commits on Apr 8, 2025

• feat(Analysis/InnerProductSpace): Add `HilbertSpace` variable alias (#23817)

  Show description for d527147
  IvanRenison

  committed
  d527147

  Copy full SHA for d527147

Commits on Feb 4, 2025

• chore(Combinatorics/SimpleGraph): Fix `hadj` naming (#21389)

  IvanRenison

  committed
  b08254c

  Copy full SHA for b08254c

Commits on Jan 27, 2025

• feat(Combinatorics/SimpleGraph): add definitions and theorems about the coloring of sum graphs (#18677)

  IvanRenison

  committed
  da67df3

  Copy full SHA for da67df3

Commits on Jan 22, 2025

• feat(Combinatorics/SimpleGraph): chromatic number of cycle graph (#20117)

  IvanRenison

  committed
  95dba76

  Copy full SHA for 95dba76

Commits on Dec 16, 2024

• chore(Algebra/Group/Nat): Remove some unnecessary lemmas arguments (#19981)

  IvanRenison

  committed
  d3319ca

  Copy full SHA for d3319ca

Commits on Dec 13, 2024

• feat(Combinatorics/SimpleGraph): Add theorem `two_le_chromaticNumber_of_adj` (#19924)

  IvanRenison

  committed
  0310194

  Copy full SHA for 0310194

Commits on Dec 10, 2024

• feat(Data/Fin): Add lemmas `Fin.odd_add_one_iff_even` and `Fin.even_add_one_iff_odd` (#19815)

  IvanRenison

  committed
  8782865

  Copy full SHA for 8782865

Commits on Nov 21, 2024

• feat(Algebra/Ring/Parity): Add lemmas `Odd.add_one` and `Odd.one_add` (#19272)

  IvanRenison

  committed
  1d199de

  Copy full SHA for 1d199de

Commits on Nov 14, 2024

• feat(Data/Fin): Add lemmas `Fin.not_odd_iff_even_of_even` and `Fin.not_even_iff_odd_of_even` (#18960)

  IvanRenison

  committed
  6d29418

  Copy full SHA for 6d29418

Commits on Nov 13, 2024

• feat(Data/Fin): Add lemmas `Fin.even_iff_mod_of_even` and `Fin.odd_iff_mod_of_even` (#18941)

  IvanRenison

  committed
  a98955e

  Copy full SHA for a98955e

Commits on Nov 4, 2024

• feat(Combinatorics/SimpleGraph): Add definition of disjoint sum of graphs (#15546)

  Show description for b44c63b
  

  IvanRenison

  and

  urkud

  committed
  b44c63b

  Copy full SHA for b44c63b

Pagination

Previous

Next