Commit 2025-05-09 11:18 5c0b9cfd

chore(NumberField/Units): make torsionOrder a Nat and prove that it is even (#23440) Originally, the order of the torsion subgroup of units of a number field was defined as a PNat since rootsOfUnity was using PNat. This is not the case anymore since rootsOfUnity is now using NeZero instead. Thus, we change the type of torsionOrder to Nat and add a NeZero instance. As a bonus, we also prove that torsionOrder is even. This PR is part of the proof of the Analytic Class Number Formula.