NumberField.Units.basisModTorsion

1000+ list: Dirichlet's unit theorem

(K : Type u_1) →
  [inst : Field K] →
    [inst_1 : NumberField K] →
      Module.Basis (Fin (NumberField.Units.rank K)) ℤ
        (Additive ((NumberField.RingOfIntegers K)ˣ ⧸ NumberField.Units.torsion K))

A basis of the quotient (𝓞 K)ˣ ⧸ (torsion K) seen as an additive ℤ-module.

Defined in: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Cited by: 4 results in Mathlib
Foundations: Depth 323 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Field NumberField

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites13

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Fieldstatement and proof · cited by 7,404
Subgroupstatement · cited by 3,593
Unitsstatement and proof · cited by 2,804
HasQuotient.Quotientstatement and proof · cited by 2,301
Module.Basisstatement · cited by 1,477
NumberFieldstatement and proof · cited by 653
NumberField.RingOfIntegersstatement and proof · cited by 413
Additivestatement and proof · cited by 356
Module.Free.chooseBasisproof · cited by 121
Module.Basis.reindexproof · cited by 57
NumberField.Units.torsionstatement and proof · cited by 53
NumberField.Units.rankstatement · cited by 46

Cited by6

Results whose statement or proof uses this declaration.

NumberField.Units.fundSystemproof · cited by 23
NumberField.Units.basisUnitLatticeproof · cited by 16
NumberField.Units.logEmbedding_fundSystemproof · cited by 4
NumberField.Units.exist_unique_eq_mul_prodproof · cited by 2
NumberField.Units.fun_eq_reprstatement and proof · cited by 1
NumberField.Units.fundSystem_mkstatement and proof · cited by 1