The order of 3 modulo 5 is four
ProvedOddPerfectNumber.order_three_mod_five_eq_fourodd-perfectorderzmod
The residue class of 3 modulo 5 has multiplicative order 4.
Preamble
import Mathlib
Formal statement
namespace OddPerfectNumber
theorem order_three_mod_five_eq_four :
orderOf (3 : ZMod 5) = 4 := by
sorry
end OddPerfectNumberSource
Finite order certificate by orderOf_eq_iff and exact ZMod arithmetic.