ScalarGeneratedGrid.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The projection obstruction once a finite coefficient closure covers an actual grid, under the covering hypothesis for the coefficient closure.