Commit 2025-05-23 17:11 06d29195

feat(NumberField/Units): add regOfFamily and refactor regulator (#22882) This is a refactor of NumberField.regulator. We introduce regOfFamily which is the regulator of a family of units indexed by Fin (Units.rank K). It is equal to 0 if the family is not isMaxRank. This is a Prop that says that the image of the family in the logSpace K is linearly independent and thus generates a full lattice. All the results about computing the regulator by some matrix determinant computation are now proved more generally for regOfFamily. The regulator of a number field is still defined as the covolume of the unitLattice and we prove that is is also equal to regOfFamily of the system of fundamental units fundSystem K. Together with the results about computing regOfFamily, we recover that way the results about computing the regulator.