Theorems · Definition · number theory

NumberField.Units.equivFinRank

(K : Type u_1) →
  [inst : Field K] →
    [inst_1 : NumberField K] → Fin (NumberField.Units.rank K) ≃ { w // w ≠ NumberField.Units.dirichletUnitTheorem.w₀ }

An equiv between Fin (rank K), used to index the family of units, and {w // w ≠ w₀} the index of the logSpace.

Defined in

Mathlib.NumberTheory.NumberField.Units.Regulator

Cited by

5 results in Mathlib

Foundations

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

Assumes

FieldNumberField