Theorems · Definition · number theory
NumberField.Units.dirichletUnitTheorem.logSpace
(K : Type u_1) → [inst : Field K] → [NumberField K] → Type (max 0 u_1)
The logSpace is defined as {w : InfinitePlace K // w ≠ w₀} → ℝ where w₀ is the
distinguished infinite place.
- Cited by
- 46 results in Mathlib
- Foundations
- Depth 298 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.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realproof · cited by 25,697
- Fieldstatement and proof · cited by 7,404
- NumberFieldstatement and proof · cited by 653
- NumberField.InfinitePlaceproof · cited by 604
- NumberField.Units.dirichletUnitTheorem.w₀proof · cited by 72
Cited by53
Results whose statement or proof uses this declaration.
- NumberField.Units.logEmbeddingstatement · cited by 25
- NumberField.Units.unitLatticestatement · cited by 21
- NumberField.mixedEmbedding.logMapstatement · cited by 21
- NumberField.Units.basisUnitLatticestatement · cited by 16
- NumberField.Units.basisOfIsMaxRankstatement · cited by 9
- NumberField.Units.regulator_eq_regOfFamily_fundSystemproof · cited by 7
- NumberField.Units.isMaxRank_fundSystemproof · cited by 4
- NumberField.Units.logEmbeddingEquivstatement · cited by 4
- NumberField.Units.logEmbedding_fundSystemstatement and proof · cited by 4
- NumberField.Units.regOfFamily_of_isMaxRankstatement · cited by 4
- NumberField.Units.regOfFamily_eq_det'statement and proof · cited by 3
- NumberField.Units.basisOfIsMaxRank_applystatement · cited by 3