Zulip Chat Archive

Stream: ABC-Exceptions

Topic: Proposition 2.6

Bhavik Mehta (May 29 2025 at 14:39):

I'm looking at the (blueprint) prop 2.6 which is refinedCountTriplesStar_isBigO_B in Lean; I'm not seeing the bit about c being coprime?

Arend Mellendijk (Jun 02 2025 at 15:30):

This is resolved in this PR

Last updated: Dec 20 2025 at 21:32 UTC