theorem
MathlibNt.SieveTheory.lemma132_finiteLayerHatUniform_slack
{H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers}
(hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H)
:
Suzuki Lemma 13.2 with one constant for every finite depth and every point of its full parity domain.
Inspect dependencies
MathlibNt.SieveTheory.lemma132_finiteLayerHatUniform_slack ยท compiled type and proof/definition references.