Code

Update GridStructure#16

Code

Closed

pitmonticone wants to merge 3 commits intofpvandoorn:masterfpvandoorn/carleson:masterfrom pitmonticone:grid-structurepitmonticone/carleson:grid-structureCopy head branch name to clipboard

+46-17

Commits

Commits on May 11, 2024

• Update GridStructure

  Show description for 6ed9e12
  pitmonticone

  committed
  6ed9e12

  Copy full SHA for 6ed9e12

Commits on May 13, 2024

• Merge pull request #1 from fpvandoorn/master

  Show description for 006846a
  pitmonticone

  authored
  006846a

  Copy full SHA for 006846a

• Update Defs.lean

  pitmonticone

  committed
  7c6b9b9

  Copy full SHA for 7c6b9b9