Theorems · Theorem · number theory

NumberField.Units.regOfFamily_div_regulator

∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  (u : Fin (NumberField.Units.rank K) → (NumberField.RingOfIntegers K)ˣ),
  NumberField.Units.regOfFamily u / NumberField.Units.regulator K =
    ↑(Subgroup.closure (Set.range u) ⊔ NumberField.Units.torsion K).index

Let u be a family of units. Then the ratio regOfFamily u / regulator K is equal to the index of the subgroup generated by u and torsion K inside the group of units of K.

Defined in

Mathlib.NumberTheory.NumberField.Units.Regulator

Cited by

1 results in Mathlib

Foundations

Depth 330 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldNumberField