Code

chore: golf a bit#293

Code

Merged

pitmonticone merged 18 commits intomasterHEPLean/HepLean:masterfrom pitmonticone/golfHEPLean/HepLean:pitmonticone/golfCopy head branch name to clipboardJan 23, 2025

+161-312

Commits

Commits on Jan 22, 2025

• Update ToSols.lean

  pitmonticone

  committed
  f91f535

  Copy full SHA for f91f535

• Update Involutions.lean

  pitmonticone

  committed
  29f55e5

  Copy full SHA for 29f55e5

• Update List.lean

  pitmonticone

  committed
  7025a29

  Copy full SHA for 7025a29

• Update InsertionSort.lean

  pitmonticone

  committed
  dd66b00

  Copy full SHA for dd66b00

• Update Insert.lean

  pitmonticone

  committed
  3447a2f

  Copy full SHA for 3447a2f

• Update InsertList.lean

  pitmonticone

  committed
  b078f63

  Copy full SHA for b078f63

• Update Sign.lean

  pitmonticone

  committed
  a328a9e

  Copy full SHA for a328a9e

• Update WicksTheorem.lean

  pitmonticone

  committed
  0cc03c0

  Copy full SHA for 0cc03c0

Commits on Jan 23, 2025

• Update LineInCubic.lean

  pitmonticone

  committed
  748188f

  Copy full SHA for 748188f

• Update LineInCubic.lean

  pitmonticone

  committed
  6589b45

  Copy full SHA for 6589b45

• Update Basic.lean

  pitmonticone

  committed
  61137e2

  Copy full SHA for 61137e2

• Update StandardParameters.lean

  pitmonticone

  committed
  291f97e

  Copy full SHA for 291f97e

• Update Boosts.lean

  pitmonticone

  committed
  06de6fe

  Copy full SHA for 06de6fe

• Update Basic.lean

  pitmonticone

  committed
  5b2a36e

  Copy full SHA for 5b2a36e

• Update NormalOrder.lean

  pitmonticone

  committed
  5055635

  Copy full SHA for 5055635

• Update NormalOrder.lean

  pitmonticone

  committed
  bd35e55

  Copy full SHA for bd35e55

• Update NormalOrder.lean

  pitmonticone

  committed
  7bbe035

  Copy full SHA for 7bbe035

• fix lint

  pitmonticone

  committed
  902434c

  Copy full SHA for 902434c