Commits

Branch selector

 master

User selector

All users

Datepicker

All time

Commit History

Commits on Oct 10, 2025

• feat: C⋆-algebras are spanned by their unitary elements (#30308)

  j-loreaux

  committed
  81a5aaa

  Copy full SHA for 81a5aaa

Commits on Oct 9, 2025

• chore: drastically speed up `LieModule.Cohomology.d₂₃` (#30377)

  Show description for 6955cd0
  

  ocfnash

  and

  Vierkantor

  committed
  6955cd0

  Copy full SHA for 6955cd0

• chore(CategoryTheory/Presentable/IsCardinalFiltered): fix name (#30306)

  Show description for d71aff6
  joelriou

  committed
  d71aff6

  Copy full SHA for d71aff6

• chore(*): rename note 'CategoryTheory universes' to 'category theory universes' (#30360)

  Show description for d12bacd
  Vierkantor

  committed
  d12bacd

  Copy full SHA for d12bacd

• feat: the Laplacian in Real is the second derivative (#30384)

  Show description for a2e710e
  RemyDegenne

  committed
  a2e710e

  Copy full SHA for a2e710e

• chore: use `fun_prop` in Homeomorph (#28929)

  Show description for 8b55e79
  grunweg

  committed
  8b55e79

  Copy full SHA for 8b55e79

• chore(Topology): some more fun_prop tagging (#23137)

  grunweg

  committed
  14871d5

  Copy full SHA for 14871d5

• feat(Analysis/Polynomial/MahlerMeasure): add a couple of easy facts (#30370)

  Show description for 7014959
  fbarroero

  committed
  7014959

  Copy full SHA for 7014959

• feat(LinearAlgebra): roots of charpoly are the eigenvalues/spectrum (#29478)

  Show description for afac0c2
  

  llllvvuu

  and

  Aristotle-Harmonic

  committed
  afac0c2

  Copy full SHA for afac0c2

• feat(Order/ScottContinuity): Scott continuity on product spaces (#26338)

  Show description for 16d3e09
  

  mans0954

  and

  YaelDillies

  committed
  16d3e09

  Copy full SHA for 16d3e09

• feat(Cardinal/Finite): ENat powers and cardinality (#27216)

  Show description for 724a6cb
  D-Thomine

  committed
  724a6cb

  Copy full SHA for 724a6cb

• feat: `UniformEquiv.subtype` (#30361)

  Show description for 0d2a45f
  smmercuri

  committed
  0d2a45f

  Copy full SHA for 0d2a45f

• feat(IsCyclotomicExtension): some results for the sub-algebra case (#29665)

  Show description for cc0d5cb
  

  xroblot

  and

  ocfnash

  committed
  cc0d5cb

  Copy full SHA for cc0d5cb

• chore (Topology/UniformSpace/Ultra): deprecate `IsTransitiveRel.mem_filter_prod_comm` (#30319)

  euprunin

  committed
  b7b295a

  Copy full SHA for b7b295a

• feat(AlgebraicTopology/SimplicialSet): nondegenerate simplices in the standard simplex (#28395)

  Show description for 946a829
  joelriou

  committed
  946a829

  Copy full SHA for 946a829

• feat: interpret `HasTemperateGrowth` in terms of `IsBigO` (#30251)

  Show description for e11b36c
  ADedecker

  committed
  e11b36c

  Copy full SHA for e11b36c

• feat(GroupTheory): add DivisibleHull (#29275)

  Show description for 6a1dc6b
  wwylele

  committed
  6a1dc6b

  Copy full SHA for 6a1dc6b

• chore(Topology/Category): golf entire `finiteCoproduct.ι_desc_apply`, `piIsoPi_hom_apply`, `prodIsoProd_hom_apply` and `pullbackIsoProdSubtype_hom_apply` using `tauto` and `rfl` (#28574)

  Show description for b68e7aa
  euprunin

  committed
  b68e7aa

  Copy full SHA for b68e7aa

• refactor: make library notes a definition (#23767)

  Show description for d554a18
  

  grunweg

  and

  Vierkantor

  committed
  d554a18

  Copy full SHA for d554a18

• feat(Geometry/Euclidean/Incenter): touchpoints in `interior` and `Sbtw` (#29837)

  Show description for 14d639d
  

  jsm28

  and

  eric-wieser

  committed
  14d639d

  Copy full SHA for 14d639d

• feat(AlgebraicTopology): the type of non degenerate simplices of a simplicial set (#28224)

  Show description for 66ed00a
  joelriou

  committed
  66ed00a

  Copy full SHA for 66ed00a

• feat(Combinatorics/Additive/VerySmallDoubling): weak non-commutative Kneser's theorem (#26660)

  Show description for 4d783e9
  

  strihanje01

  and

  YaelDillies

  committed
  4d783e9

  Copy full SHA for 4d783e9

• feat(Algebra/Group/Submonoid): add `(Add)Submonoid.closure_pi` (#29823)

  Show description for 3305d4b
  themathqueen

  committed
  3305d4b

  Copy full SHA for 3305d4b

• feat(Geometry/Euclidean/Angle/Bisector): bisecting angles and equal distances (#29656)

  Show description for 917d337
  jsm28

  committed
  917d337

  Copy full SHA for 917d337

• feat: remove separability assumption from Algebra.isIntegral_norm (#30323)

  Show description for 1ed2bab
  riccardobrasca

  committed
  1ed2bab

  Copy full SHA for 1ed2bab

• feat(Data/Nat/BinaryRec): equational lemmas for variants of binary recursion (#30221)

  Show description for 03556d0
  b-mehta

  committed
  03556d0

  Copy full SHA for 03556d0

• feat: Fernique's theorem for Gaussian distributions (#30167)

  Show description for dc9234a
  RemyDegenne

  committed
  dc9234a

  Copy full SHA for dc9234a

• feat: composing a continuous multilinear map with continuous linear maps is analytic in both variables (#30111)

  Show description for 67f5eec
  

  sgouezel

  and

  pre-commit-ci-lite[bot]

  committed
  67f5eec

  Copy full SHA for 67f5eec

• chore: move some results from `Analysis/Normed/Algebra/Spectrum` to `Analysis/{Real, Complex}/Spectrum` (#29916)

  themathqueen

  committed
  760bc88

  Copy full SHA for 760bc88

• chore(Algebra/Order/BigOperators/Group/{Finset, Multiset}): generalize results to `(Mul)(Add)LeftMono` (#29864)

  Show description for 6011733
  themathqueen

  committed
  6011733

  Copy full SHA for 6011733

• feat(Algebra/HahnEmbedding): ArchimedeanStrata is non-empty (#30101)

  Show description for 41c5057
  wwylele

  committed
  41c5057

  Copy full SHA for 41c5057

• feat: the Hölder conjugate of an `ENNReal` (#30174)

  mcdoll

  committed
  5592362

  Copy full SHA for 5592362

• chore(SimpleGraph/Subgraph): remove duplicate def and fix names (#29690)

  Show description for 0b0ba00
  jt496

  committed
  0b0ba00

  Copy full SHA for 0b0ba00

Commits on Oct 8, 2025

• feat (Algebra/Lie): Define low-degree cochains and differentials (#29154)

  Show description for 3540854
  ScottCarnahan

  committed
  3540854

  Copy full SHA for 3540854

• feat (TopCat.Sphere) : add the open ball, instances (#29789)

  Show description for 9ccce5c
  robertmaxton42

  committed
  9ccce5c

  Copy full SHA for 9ccce5c

Pagination

Previous

Next