Documentation Verification Report

AdeleRing

📁 Source: FLT/NumberField/AdeleRing.lean

Statistics

Metric	Count
Definitions `toAdicCompletion`, `ModuleBaseChangeAddEquiv`, `ModuleBaseChangeAddEquiv'`, `ModuleBaseChangeContinuousAddEquiv`, `ModuleBaseChangeContinuousSemilinearMap`, `baseChange`, `baseChangeAdeleAlgEquiv`, `baseChangeAdeleAlgHom`, `baseChangeAdeleEquiv`, `baseChangeAlgAdeleEquiv`, `baseChangeEquiv`, `baseChangeSemialgHom`, `instAlgebraRingOfIntegers_fLT`, `instAlgebraRingOfIntegers_fLT_1`, `piEquiv`, `piQuotientEquiv`, `tensorProductEquivPi`, `term𝔸_`, `fundamentalDomain`, `padicEquiv`, `instVAddRatAdeleRingRingOfIntegers_fLT`	21
Theorems `ModuleBaseChangeAddEquiv_apply`, `ModuleBaseChangeContinuousSemilinearMap_apply`, `baseChangeAdeleAlgEquiv_apply`, `baseChangeAdeleAlgHom_bijective`, `baseChangeEquiv_tsum_apply_right`, `cocompact`, `comap_piEquiv_principalSubgroup`, `discrete`, `instBaseChangeIsModuleTopology`, `instFiniteRingOfIntegers_fLT`, `instIsScalarTowerRingOfIntegers_fLT`, `instPiIsModuleTopology`, `moduleBaseChangeContinuousAddEquiv_apply_eq_moduleBaseChangeAddEquiv'_apply`, `piEquiv_apply_of_algebraMap`, `piEquiv_map_principalSubgroup`, `piEquiv_mem_principalSubgroup`, `zero_discrete`, `cocompact`, `fundamentalDomain_traversal`, `integral_and_norm_lt_one`, `isAddFundamentalDomain`, `mem_fundamentalDomain`, `zero_discrete`, `instFactPrimeValNat_fLT`, `padicEquiv_bijOn`, `sub_mem_integralAdeles`, `exists_sub_norm_le_one`, `exists_unique_sub_mem_Ico`, `instProperSpaceCompletion_fLT`	29
Total	50

FiniteAdeleRing

Definitions

Name	Category	Theorems
`toAdicCompletion` 📖	CompOp	—

NumberField.AdeleRing

Definitions

Name	Category	Theorems
`ModuleBaseChangeAddEquiv` 📖	CompOp	1 math math: `ModuleBaseChangeAddEquiv_apply`
`ModuleBaseChangeAddEquiv'` 📖	CompOp	1 math math: `moduleBaseChangeContinuousAddEquiv_apply_eq_moduleBaseChangeAddEquiv'_apply`
`ModuleBaseChangeContinuousAddEquiv` 📖	CompOp	1 math math: `moduleBaseChangeContinuousAddEquiv_apply_eq_moduleBaseChangeAddEquiv'_apply`
`ModuleBaseChangeContinuousSemilinearMap` 📖	CompOp	1 math math: `ModuleBaseChangeContinuousSemilinearMap_apply`
`baseChange` 📖	CompOp	—
`baseChangeAdeleAlgEquiv` 📖	CompOp	1 math math: `baseChangeAdeleAlgEquiv_apply`
`baseChangeAdeleAlgHom` 📖	CompOp	1 math math: `baseChangeAdeleAlgHom_bijective`
`baseChangeAdeleEquiv` 📖	CompOp	—
`baseChangeAlgAdeleEquiv` 📖	CompOp	—
`baseChangeEquiv` 📖	CompOp	1 math math: `baseChangeEquiv_tsum_apply_right`
`baseChangeSemialgHom` 📖	CompOp	—
`instAlgebraRingOfIntegers_fLT` 📖	CompOp	52 math math: `DivisionAlgebra.Aux.T_finite_extracted1`, `Rat.AdeleRing.mem_fundamentalDomain`, `MeasureTheory.addHaarScalarFactor_tensor_adeles_eq_one`, `ModuleBaseChangeContinuousSemilinearMap_apply`, `DivisionAlgebra.Aux.compact_includeLeft_subgroup`, `DivisionAlgebra.Aux.C_compact`, `DivisionAlgebra.Aux.X_compact`, `DivisionAlgebra.Aux.incl_D𝔸quot_surjective`, `DivisionAlgebra.Aux.Y_compact`, `piEquiv_map_principalSubgroup`, `DivisionAlgebra.Aux.ringHaarChar_D𝔸`, `DivisionAlgebra.Aux.incl_D𝔸quot_continuous`, `DivisionAlgebra.Aux.discrete_includeLeft_subgroup`, `DivisionAlgebra.Aux.E_family_compact`, `DivisionAlgebra.Aux.smul_D𝔸_prodRight_symm`, `Rat.AdeleRing.zero_discrete`, `ModuleBaseChangeAddEquiv_apply`, `DivisionAlgebra.Aux.E_compact`, `DivisionAlgebra.Aux.toQuot_cont`, `baseChangeEquiv_tsum_apply_right`, `DivisionAlgebra.Aux.instBorelSpaceTensorProductRingOfIntegers_fLT`, `instIsScalarTowerRingOfIntegers_fLT`, `units_mem_ringHaarCharacter_ker`, `DivisionAlgebra.Aux.ImAux_isCompact`, `DivisionAlgebra.Aux.toQuot_surjective`, `isCentralSimple_addHaarScalarFactor_left_mul_eq_right_mul`, `DivisionAlgebra.Aux.not_injective_of_large_measure`, `addEquivAddHaarChar_mulRight_unit_eq_one`, `discrete`, `comap_piEquiv_principalSubgroup`, `MeasureTheory.ringHaarChar_adeles_units_rat_eq_one`, `DivisionAlgebra.Aux.T_finite`, `MeasureTheory.addHaarScalarFactor_tensor_adeles_rat_eq_one`, `DivisionAlgebra.Aux.D𝔸_prodRight_units_cont`, `DivisionAlgebra.Aux.ringHaarChar_D𝔸_prodRight_units_aux`, `DivisionAlgebra.Aux.instT2SpaceTensorProductRingOfIntegers_fLT`, `baseChangeAdeleAlgEquiv_apply`, `DivisionAlgebra.compact_quotient`, `moduleBaseChangeContinuousAddEquiv_apply_eq_moduleBaseChangeAddEquiv'_apply`, `DivisionAlgebra.Aux.rest₁_surjective`, `DivisionAlgebra.Aux.rest₁_continuous`, `DivisionAlgebra.Aux.ringHaarChar_D𝔸_real_surjective`, `DivisionAlgebra.Aux.M_compact`, `zero_discrete`, `DivisionAlgebra.Aux.incl₂_isClosedEmbedding`, `piEquiv_mem_principalSubgroup`, `DivisionAlgebra.Aux.E_family_unbounded`, `baseChangeAdeleAlgHom_bijective`, `DivisionAlgebra.Aux.E_family_nonempty_interior`, `DivisionAlgebra.Aux.D_discrete`, `DivisionAlgebra.Aux.D_discrete_aux`, `DivisionAlgebra.Aux.existsE`
`instAlgebraRingOfIntegers_fLT_1` 📖	CompOp	6 math math: `ModuleBaseChangeContinuousSemilinearMap_apply`, `instBaseChangeIsModuleTopology`, `ModuleBaseChangeAddEquiv_apply`, `baseChangeAdeleAlgEquiv_apply`, `instFiniteRingOfIntegers_fLT`, `baseChangeAdeleAlgHom_bijective`
`piEquiv` 📖	CompOp	4 math math: `piEquiv_apply_of_algebraMap`, `piEquiv_map_principalSubgroup`, `comap_piEquiv_principalSubgroup`, `piEquiv_mem_principalSubgroup`
`piQuotientEquiv` 📖	CompOp	—
`tensorProductEquivPi` 📖	CompOp	—
`term𝔸_` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ModuleBaseChangeAddEquiv_apply` 📖	mathematical	—	`instAlgebraRingOfIntegers_fLT` `ModuleBaseChangeAddEquiv` `instAlgebraRingOfIntegers_fLT_1`	—	`baseChangeAdeleAlgEquiv_apply`
`ModuleBaseChangeContinuousSemilinearMap_apply` 📖	mathematical	—	`instAlgebraRingOfIntegers_fLT_1` `instAlgebraRingOfIntegers_fLT` `TensorProduct.RightActions.instModule_fLT` `ModuleBaseChangeContinuousSemilinearMap`	—	`ModuleBaseChangeAddEquiv_apply`
`baseChangeAdeleAlgEquiv_apply` 📖	mathematical	—	`instAlgebraRingOfIntegers_fLT` `baseChangeAdeleAlgEquiv` `instAlgebraRingOfIntegers_fLT_1`	—	—
`baseChangeAdeleAlgHom_bijective` 📖	mathematical	—	`instAlgebraRingOfIntegers_fLT` `TensorProduct.RightActions.instAlgebra_fLT` `instAlgebraRingOfIntegers_fLT_1` `baseChangeAdeleAlgHom`	—	`TensorProduct.RightActions.instIsScalarTower_fLT` `instIsScalarTowerRingOfIntegers_fLT`
`baseChangeEquiv_tsum_apply_right` 📖	mathematical	—	`instAlgebraRingOfIntegers_fLT` `TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT` `baseChangeEquiv`	—	—
`cocompact` 📖	—	—	—	—	`Rat.AdeleRing.cocompact`
`comap_piEquiv_principalSubgroup` 📖	mathematical	—	`instAlgebraRingOfIntegers_fLT` `piEquiv`	—	`piEquiv_map_principalSubgroup`
`discrete` 📖	mathematical	—	`instAlgebraRingOfIntegers_fLT`	—	`zero_discrete` `Homeomorph.subLeft.congr_simp`
`instBaseChangeIsModuleTopology` 📖	mathematical	—	`instAlgebraRingOfIntegers_fLT_1`	—	`IsModuleTopology.instProd'` `NumberField.InfiniteAdeleRing.instIsModuleTopology_fLT` `IsDedekindDomain.instIsModuleTopologyFiniteAdeleRing_fLT`
`instFiniteRingOfIntegers_fLT` 📖	mathematical	—	`instAlgebraRingOfIntegers_fLT_1`	—	`TensorProduct.RightActions.instFinite_fLT`
`instIsScalarTowerRingOfIntegers_fLT` 📖	mathematical	—	`instAlgebraRingOfIntegers_fLT`	—	—
`instPiIsModuleTopology` 📖	—	—	—	—	—
`moduleBaseChangeContinuousAddEquiv_apply_eq_moduleBaseChangeAddEquiv'_apply` 📖	mathematical	—	`instAlgebraRingOfIntegers_fLT` `TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT` `ModuleBaseChangeContinuousAddEquiv` `TensorProduct.RightActions.instModule_fLT` `ModuleBaseChangeAddEquiv'`	—	—
`piEquiv_apply_of_algebraMap` 📖	mathematical	`instAlgebraRingOfIntegers_fLT`	`piEquiv` `Module.Finite.equivPi`	—	`TensorProduct.AlgebraTensorModule.finiteEquivPi_symm_apply` `TensorProduct.RightActions.Algebra.TensorProduct.comm_apply_tmul` `baseChangeEquiv_tsum_apply_right`
`piEquiv_map_principalSubgroup` 📖	mathematical	—	`instAlgebraRingOfIntegers_fLT` `piEquiv`	—	`piEquiv_mem_principalSubgroup` `piEquiv_apply_of_algebraMap`
`piEquiv_mem_principalSubgroup` 📖	mathematical	—	`instAlgebraRingOfIntegers_fLT` `piEquiv`	—	`piEquiv_apply_of_algebraMap`
`zero_discrete` 📖	mathematical	—	`instAlgebraRingOfIntegers_fLT`	—	`Rat.AdeleRing.zero_discrete` `piEquiv_apply_of_algebraMap`

Rat.AdeleRing

Definitions

Name	Category	Theorems
`fundamentalDomain` 📖	CompOp	2 math math: `mem_fundamentalDomain`, `isAddFundamentalDomain`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cocompact` 📖	—	—	—	—	`instProperSpaceCompletion_fLT` `instCompactSpaceSubtypeFiniteAdeleRingRingOfIntegersMemSubringIntegralAdeles` `RestrictedProduct.mem_structureSubring_iff` `Rat.InfiniteAdeleRing.exists_sub_norm_le_one` `Rat.FiniteAdeleRing.sub_mem_integralAdeles`
`fundamentalDomain_traversal` 📖	—	`fundamentalDomain` `NumberField.AdeleRing.instAlgebraRingOfIntegers_fLT`	—	—	`integral_and_norm_lt_one` `Rat.infinitePlace_isReal`
`integral_and_norm_lt_one` 📖	—	`IsDedekindDomain.baseChangeAlgebra` `NumberField.InfiniteAdeleRing.instAlgebra_fLT_1`	—	—	—
`isAddFundamentalDomain` 📖	mathematical	—	`instVAddRatAdeleRingRingOfIntegers_fLT` `instMeasurableSpaceCompletion_fLT` `instMeasurableSpaceFiniteAdeleRingRingOfIntegers_fLT` `fundamentalDomain` `instBorelSpaceCompletion_fLT` `instBorelSpaceFiniteAdeleRingRingOfIntegers_fLT` `instLocallyCompactSpaceFiniteAdeleRingRingOfIntegers_fLT`	—	`instBorelSpaceCompletion_fLT` `instBorelSpaceFiniteAdeleRingRingOfIntegers_fLT` `instLocallyCompactSpaceFiniteAdeleRingRingOfIntegers_fLT` `Rat.infinitePlace_isReal` `NumberField.isOpenAdicCompletionIntegers` `mem_fundamentalDomain` `fundamentalDomain_traversal`
`mem_fundamentalDomain` 📖	mathematical	—	`fundamentalDomain` `NumberField.AdeleRing.instAlgebraRingOfIntegers_fLT`	—	`Rat.FiniteAdeleRing.sub_mem_integralAdeles` `Rat.infinitePlace_isReal` `Rat.InfiniteAdeleRing.exists_unique_sub_mem_Ico`
`zero_discrete` 📖	mathematical	—	`NumberField.AdeleRing.instAlgebraRingOfIntegers_fLT`	—	`integral_and_norm_lt_one`

Rat.FiniteAdeleRing

Definitions

Name	Category	Theorems
`padicEquiv` 📖	CompOp	1 math math: `padicEquiv_bijOn`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instFactPrimeValNat_fLT` 📖	—	—	—	—	—
`padicEquiv_bijOn` 📖	mathematical	—	`instFactPrimeValNat_fLT` `IsDedekindDomain.baseChangeAlgebra` `RestrictedProduct.instAlgebraRatPrimesPadicValNatPrimeCoeSubringSubringCofinite_fLT` `padicEquiv` `IsDedekindDomain.FiniteAdeleRing.integralAdeles` `RestrictedProduct.structureSubring`	—	`RingEquiv.restrictedProductCongr_bijOn_structureSubring` `instFactPrimeValNat_fLT`
`sub_mem_integralAdeles` 📖	mathematical	—	`IsDedekindDomain.FiniteAdeleRing.integralAdeles` `IsDedekindDomain.baseChangeAlgebra`	—	`RestrictedProduct.instFactPrimeValNat_fLT` `instFactPrimeValNat_fLT` `RestrictedProduct.padic_exists_sub_mem_structureSubring` `padicEquiv_bijOn`

Rat.InfiniteAdeleRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_sub_norm_le_one` 📖	mathematical	—	`NumberField.InfiniteAdeleRing.instAlgebra_fLT_1`	—	`Rat.infinitePlace_isReal` `exists_unique_sub_mem_Ico`
`exists_unique_sub_mem_Ico` 📖	—	—	—	—	`Rat.infinitePlace_isReal` `Rat.ringOfIntegersEquiv_symm_coe` `Int.eq_floor`

(root)

Definitions

Name	Category	Theorems
`instVAddRatAdeleRingRingOfIntegers_fLT` 📖	CompOp	1 math math: `Rat.AdeleRing.isAddFundamentalDomain`

Theorems

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

---

← Back to Index