Zulip Chat Archive

Stream: Is there code for X?

Topic: norm_num for orderOf

Riccardo Brasca (May 27 2025 at 09:34):

Does anyone have a norm_num extension that computes orderOf (ZMod.unitOfCoprime a h) where (a b : ℕ) (h : a.Coprime b)?

Riccardo Brasca (May 27 2025 at 09:35):

(of course a more general version that works in finite groups would be even better)

Last updated: Dec 20 2025 at 21:32 UTC