Theorems · Definition · number theory
NumberField.Units.regOfFamily
{K : Type u_1} →
[inst : Field K] → [inst_1 : NumberField K] → (Fin (NumberField.Units.rank K) → (NumberField.RingOfIntegers K)ˣ) → ℝThe regulator of a family of units of K.
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 304 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.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Realstatement · cited by 25,697
- Fieldstatement and proof · cited by 7,404
- Set.rangeproof · cited by 4,705
- Unitsstatement and proof · cited by 2,804
- Submodule.spanproof · cited by 1,504
- MeasureTheory.MeasureSpace.volumeproof · cited by 1,323
- NumberFieldstatement and proof · cited by 653
- NumberField.RingOfIntegersstatement and proof · cited by 413
- NumberField.Units.rankstatement and proof · cited by 46
- ZLattice.covolumeproof · cited by 21
- NumberField.Units.IsMaxRankproof · cited by 12
Cited by12
Results whose statement or proof uses this declaration.
- NumberField.Units.regulator_eq_regOfFamily_fundSystemstatement · cited by 7
- NumberField.Units.regOfFamily_of_isMaxRankstatement · cited by 4
- NumberField.Units.regOfFamily_eq_zerostatement · cited by 3
- NumberField.Units.regOfFamily_eq_detstatement · cited by 3
- NumberField.Units.regOfFamily_eq_det'statement · cited by 3
- NumberField.Units.finrank_mul_regOfFamily_eq_detstatement and proof · cited by 2
- NumberField.Units.regOfFamily_posstatement · cited by 2
- NumberField.Units.regOfFamily_div_regulatorstatement and proof · cited by 1
- NumberField.Units.regOfFamily_div_regOfFamilystatement and proof · cited by 1
- NumberField.Units.regOfFamily_ne_zerostatement · cited by 1
- NumberField.IsCMField.regOfFamily_realFunSystemstatement and proof · cited by 1
- NumberField.Units.regOfFamily_ne_zero_iffstatement and proof · cited by 0