Theorems · Theorem · number theory
NumberField.Units.exist_unique_eq_mul_prod
- 1000+ list: Dirichlet's unit theorem
∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (x : (NumberField.RingOfIntegers K)ˣ), ∃! ζe, x = ↑ζe.1 * ∏ i, NumberField.Units.fundSystem K i ^ ζe.2 i
Dirichlet Unit Theorem. Any unit x of 𝓞 K can be written uniquely as the product of
a root of unity and powers of the units of the fundamental system fundSystem.
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 326 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- FieldNumberField
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites37
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Fieldstatement and proof · cited by 7,404
- Finset.sumproof · cited by 5,195
- Subgroupstatement · cited by 3,593
- Finset.univstatement and proof · cited by 3,473
- Unitsstatement and proof · cited by 2,804
- Finset.prodstatement and proof · cited by 2,356
- Finset.sum_congrproof · cited by 2,323
- HasQuotient.Quotientproof · cited by 2,301
- neg_negproof · cited by 960
- NumberFieldstatement and proof · cited by 653
- Finset.prod_congrproof · cited by 646
Cited by2
Results whose statement or proof uses this declaration.
- NumberField.Units.closure_fundSystem_sup_torsion_eq_topproof · cited by 2
- IsCyclotomicExtension.Rat.Three.Units.memproof · cited by 1