Commits

Branch selector

 master

User selector

urkud

Datepicker

All time

Commit History

Commits on Oct 4, 2025

• feat(NormedSpace/Alternating/Uncurry/Fin): new file (#29957)

  urkud

  committed
  b4264fb

  Copy full SHA for b4264fb

Commits on Oct 3, 2025

• feat(CharP/*): generalize a lemma, add `ringChar_eq_one` (#29952)

  urkud

  committed
  ddbd4d2

  Copy full SHA for ddbd4d2

Commits on Oct 2, 2025

• chore(Convex/Extreme): redefine `IsExtreme` and `extremePoints` (#29950)

  Show description for e793704
  urkud

  committed
  e793704

  Copy full SHA for e793704

Commits on Sep 30, 2025

• feat(TangentCone): generalize some lemmas to TVS (#29842)

  Show description for 213ff10
  urkud

  committed
  213ff10

  Copy full SHA for 213ff10

• feat(FDeriv/Analytic): generalize results about derivatives of multilinear maps (#30018)

  urkud

  committed
  9978e09

  Copy full SHA for 9978e09

• feat(Finset/Interval): improve computation performance (#30078)

  Show description for 49fa7a7
  urkud

  committed
  49fa7a7

  Copy full SHA for 49fa7a7

Commits on Sep 27, 2025

• feat(HaarToSphere): add integrability lemmas (#24248)

  urkud

  committed
  5a2fc85

  Copy full SHA for 5a2fc85

• feat(FDeriv/CompCLM): application of continuous alternating maps to constants (#29984)

  Show description for d018b27
  urkud

  committed
  d018b27

  Copy full SHA for d018b27

Commits on Sep 26, 2025

• chore(TangentCone): add 2 `simp` attributes (#29986)

  urkud

  committed
  e5a6d2d

  Copy full SHA for e5a6d2d

Commits on Sep 25, 2025

• feat(Convex/LinearIsometry): new file (#24157)

  urkud

  committed
  2f015bc

  Copy full SHA for 2f015bc

Commits on Sep 22, 2025

• feat(ConstMulAction): prove `set_smul_closure_subset` (#29859)

  Show description for 5c1fe16
  urkud

  committed
  5c1fe16

  Copy full SHA for 5c1fe16

Commits on Sep 21, 2025

• feat(Topology/Maps): `IsOpenMap` and `ClusterPt` (#23240)

  urkud

  committed
  c822477

  Copy full SHA for c822477

Commits on Sep 19, 2025

• feat(Topology/UniformSpace/Path): new file (#24105)

  urkud

  committed
  d8a594d

  Copy full SHA for d8a594d

• chore(*): drop some `Decidable`/`Fintype` assumptions (#29785)

  Show description for 85c6303
  urkud

  committed
  85c6303

  Copy full SHA for 85c6303

Commits on Sep 16, 2025

• fix(Topology/Homotopy): fix name&args order of `comp` (#24829)

  Show description for 41d6186
  urkud

  committed
  41d6186

  Copy full SHA for 41d6186

Commits on Jun 5, 2025

• feat(NormedSpace/Alternating/Curry): new file (#25469)

  urkud

  committed
  0a7d179

  Copy full SHA for 0a7d179

Commits on Jun 4, 2025

• feat(AlternatingMap): define `AlternatingMap.uncurryFin`. (#25001)

  urkud

  committed
  bf709e0

  Copy full SHA for bf709e0

Commits on Jun 2, 2025

• feat(Perm/Fin): add lemmas about `cycleRange` and `insertNth` (#24980)

  urkud

  committed
  a55b976

  Copy full SHA for a55b976

Commits on May 29, 2025

• chore(*): use `gcongr` (#25289)

  urkud

  committed
  7329910

  Copy full SHA for 7329910

Commits on May 27, 2025

• chore(*): golf using tactics (#25227)

  Show description for 88f487f
  urkud

  committed
  88f487f

  Copy full SHA for 88f487f

Commits on May 26, 2025

• chore(*): review `simp` lemmas for `piCongr*` equivs (#24493)

  Show description for cdf00c3
  urkud

  committed
  cdf00c3

  Copy full SHA for cdf00c3

Commits on May 25, 2025

• chore(*): use `gcongr`&`positivity` (#25128)

  urkud

  committed
  3537c25

  Copy full SHA for 3537c25

• chore(*): not_mem/nmem -> notMem (#25159)

  urkud

  committed
  401dce0

  Copy full SHA for 401dce0

• feat(ContinuousMap): add a LocallyConvexSpace instance (#24606)

  urkud

  committed
  6644c20

  Copy full SHA for 6644c20

• fix(Order/Field/Pointwise): use `*` in the RHS (#25047)

  Show description for 5e80da4
  urkud

  committed
  5e80da4

  Copy full SHA for 5e80da4

Commits on May 22, 2025

• chore(*): use `positivity` (#25103)

  urkud

  committed
  f34c1f5

  Copy full SHA for f34c1f5

• chore(*): use `gcongr` (#25090)

  urkud

  committed
  8599e8d

  Copy full SHA for 8599e8d

• chore(*): use `gcongr` (#25100)

  urkud

  committed
  2199bf0

  Copy full SHA for 2199bf0

• feat(IntervalIntegral): +1 version of `norm_integral_le_of_norm_le` (#25075)

  urkud

  committed
  ae78100

  Copy full SHA for ae78100

• chore(*): use `gcongr` and `omega` (#25097)

  urkud

  committed
  44f2e31

  Copy full SHA for 44f2e31

Commits on May 21, 2025

• chore(StrongLaw): use `gcongr` (#25082)

  urkud

  committed
  7ac680c

  Copy full SHA for 7ac680c

• chore(*): use `gcongr` (#25081)

  urkud

  committed
  63c9b4f

  Copy full SHA for 63c9b4f

• chore(LocallyConvexSpace): drop an unused argument (#25058)

  urkud

  committed
  3a1df12

  Copy full SHA for 3a1df12

• chore(Behrend): golf using `calc` and `gcongr` (#25074)

  Show description for dcb4edb
  urkud

  committed
  dcb4edb

  Copy full SHA for dcb4edb

• chore(*): golf, use `Matrix.mulVec` (#25072)

  Show description for 36d4490
  urkud

  committed
  36d4490

  Copy full SHA for 36d4490

Pagination

Previous

Next