Theorems · Theorem · number theory

NumberField.Units.regOfFamily_div_regOfFamily

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

Let u and v be two families of units. Assume that the subgroup U generated by u and torsion K is contained in the subgroup V generated by v and torsion K. Then the ratio regOfFamily u / regOfFamily v is equal to the index of U inside V.

Defined in

Mathlib.NumberTheory.NumberField.Units.Regulator

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldNumberField