AffineResidueAverage.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Freeze a progression class and change every prime residue by the same invertible affine map. This preserves the precise uniform model.