theorem
MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12AuthorWeight_le_eight
(u : ℝ)
:
The author weight is capped only for the exceptional divisor error.
Inspect dependencies
MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12AuthorWeight_le_eight · compiled type and proof/definition references.