is there an existing NTT proof?

Stream: mathlib4

[Jonathan Protzenko]

Wondering if anyone has an NTT (number theoretic transform) proof lying around somewhere? All I could find was https://github.com/madvorak/lean-fft/blob/81fa0e4b2a55b06a8473401cc65d43f059ef686e/NumberTheoreticTransform.lean where the proof is admitted

[Martin Dvořák]

In fact, I finished the proof in the end
https://github.com/madvorak/lean-fft/blob/main/NumberTheoreticTransform.lean
but the implementation of the algorithm is HORRIBLE.

[Martin Dvořák]

For clarification, there are more things you might want to proof; I was possibly proving something else.
I have a proof that the FFT-like NTT gives the same result as NTT calculated directly from definition.
I don't have a proof that NTT works in the sense that NTT comes with an inverse transformation.

[Jonathan Protzenko]

I forgot to respond to this -- thanks! that's quite helpful