Documentation Verification Report

RestrictedProduct

📁 Source: FLT/NumberField/Padics/RestrictedProduct.lean

Statistics

Metric	Count
Definitions `instAlgebraRatPrimesPadicValNatPrimeCoeSubringSubringCofinite_fLT`, `padicNatDen`, `padicNum`	3
Theorems `instFactPrimeValNat_fLT`, `setOf_norm_one_lt_finite`, `instFactPrimeValNat_fLT`, `padicNatDen_ne_zero`, `padicNatDen_norm_mul_le_one`, `padicNatDen_norm_of_mem`, `padicNatDen_norm_of_notMem`, `padic_exists_sub_mem_padicInt`, `padic_exists_sub_mem_structureSubring`, `padic_valuation_neg_of_mem_indexSupport`	10
Total	13

Padic

Theorems

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

RestrictedProduct

Definitions

Name	Category	Theorems
`instAlgebraRatPrimesPadicValNatPrimeCoeSubringSubringCofinite_fLT` 📖	CompOp	2 math math: `padic_exists_sub_mem_structureSubring`, `Rat.FiniteAdeleRing.padicEquiv_bijOn`
`padicNatDen` 📖	CompOp	3 math math: `padicNatDen_norm_mul_le_one`, `padicNatDen_norm_of_mem`, `padicNatDen_norm_of_notMem`
`padicNum` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instFactPrimeValNat_fLT` 📖	—	—	—	—	—
`padicNatDen_ne_zero` 📖	—	—	—	—	`instFactPrimeValNat_fLT` `padicNatDen.eq_1`
`padicNatDen_norm_mul_le_one` 📖	mathematical	—	`instFactPrimeValNat_fLT` `padicNatDen`	—	`instFactPrimeValNat_fLT` `padicNatDen_norm_of_mem` `padic_valuation_neg_of_mem_indexSupport` `padicNatDen_norm_of_notMem`
`padicNatDen_norm_of_mem` 📖	mathematical	`indexSupport` `instFactPrimeValNat_fLT`	`padicNatDen`	—	`instFactPrimeValNat_fLT` `padic_valuation_neg_of_mem_indexSupport`
`padicNatDen_norm_of_notMem` 📖	mathematical	`indexSupport` `instFactPrimeValNat_fLT`	`padicNatDen`	—	`instFactPrimeValNat_fLT`
`padic_exists_sub_mem_padicInt` 📖	mathematical	—	`instFactPrimeValNat_fLT`	—	`instFactPrimeValNat_fLT` `padicNatDen_ne_zero` `padicNatDen_norm_of_mem` `padicNatDen_norm_of_notMem`
`padic_exists_sub_mem_structureSubring` 📖	mathematical	—	`instFactPrimeValNat_fLT` `structureSubring` `instAlgebraRatPrimesPadicValNatPrimeCoeSubringSubringCofinite_fLT`	—	`instFactPrimeValNat_fLT` `padic_exists_sub_mem_padicInt` `mem_structureSubring_iff`
`padic_valuation_neg_of_mem_indexSupport` 📖	—	`indexSupport` `instFactPrimeValNat_fLT`	—	—	`instFactPrimeValNat_fLT`

---

← Back to Index