Documentation Verification Report

HeightOneSpectrum

📁 Source: FLT/Mathlib/NumberTheory/Padics/HeightOneSpectrum.lean

Statistics

Metric	Count
Definitions	0
Theorems `instFiniteInt_fLT`, `instFreeInt_fLT`, `instIsPrincipalIdealRing_fLT`, `intEquiv_apply_coe`, `padicEquiv_cast`, `padicEquiv_norm_coe_eq`, `padicEquiv_norm_eq`, `intValuation_eq_padicValuation_iff_multiplicity_eq_multiplicity`, `natGenerator_eq_absNorm`, `pow_natGenerator_dvd_iff`, `valuation_apply_coe_eq_padicValuation`, `valuation_apply_eq_padicValuation`, `instFactPrimeValNat_fLT`	13
Total	13

Rat.HeightOneSpectrum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`intValuation_eq_padicValuation_iff_multiplicity_eq_multiplicity` 📖	mathematical	—	`instFactPrimeValNat_fLT`	—	`instFactPrimeValNat_fLT` `IsDedekindDomain.HeightOneSpectrum.intValuation_eq_coe_neg_multiplicity`
`natGenerator_eq_absNorm` 📖	mathematical	—	`IsIntegralClosure.instFreeInt_fLT`	—	`IsIntegralClosure.instFreeInt_fLT` `IsIntegralClosure.instIsPrincipalIdealRing_fLT` `IsIntegralClosure.instFiniteInt_fLT` `IsIntegralClosure.intEquiv_apply_coe`
`pow_natGenerator_dvd_iff` 📖	—	—	—	—	—
`valuation_apply_coe_eq_padicValuation` 📖	mathematical	—	`instFactPrimeValNat_fLT`	—	`instFactPrimeValNat_fLT` `intValuation_eq_padicValuation_iff_multiplicity_eq_multiplicity` `pow_natGenerator_dvd_iff`
`valuation_apply_eq_padicValuation` 📖	mathematical	—	`instFactPrimeValNat_fLT`	—	`instFactPrimeValNat_fLT` `valuation_apply_coe_eq_padicValuation`

Rat.HeightOneSpectrum.IsIntegralClosure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instFiniteInt_fLT` 📖	—	—	—	—	—
`instFreeInt_fLT` 📖	—	—	—	—	—
`instIsPrincipalIdealRing_fLT` 📖	—	—	—	—	—
`intEquiv_apply_coe` 📖	—	—	—	—	—

Rat.HeightOneSpectrum.adicCompletion

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`padicEquiv_cast` 📖	—	—	—	—	—
`padicEquiv_norm_coe_eq` 📖	—	—	—	—	`padicEquiv_cast` `instFactPrimeValNat_fLT` `Rat.HeightOneSpectrum.IsIntegralClosure.instFreeInt_fLT` `Rat.HeightOneSpectrum.natGenerator_eq_absNorm` `Rat.HeightOneSpectrum.valuation_apply_eq_padicValuation`
`padicEquiv_norm_eq` 📖	—	—	—	—	`padicEquiv_norm_coe_eq`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instFactPrimeValNat_fLT` 📖	—	—	—	—	—

---

← Back to Index