AdeleRing

📁 Source: FLT/HaarMeasure/HaarChar/AdeleRing.lean

Statistics

Metric	Count
Definitions baseChange	1
Theorems baseChange_apply, toMatrix_basis, toMatrix_map_left, toMatrix_map_right, addHaarScalarFactor_tensor_adeles_eq_one, addHaarScalarFactor_tensor_adeles_rat_eq_one, ringHaarChar_adeles_rat, ringHaarChar_adeles_units_rat_eq_one, addEquivAddHaarChar_mulRight_unit_eq_one, units_mem_ringHaarCharacter_ker	10
Total	11

ContinuousLinearEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
baseChange_apply 📖	mathematical	—	TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT TensorProduct.RightActions.instModule_fLT TensorProduct.RightActions.ContinuousLinearEquiv.baseChange	—	—

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toMatrix_basis 📖	—	—	—	—	—
toMatrix_map_left 📖	—	—	—	—	—
toMatrix_map_right 📖	—	—	—	—	—

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addHaarScalarFactor_tensor_adeles_eq_one 📖	mathematical	—	NumberField.AdeleRing.instAlgebraRingOfIntegers_fLT TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT TensorProduct.RightActions.instIsTopologicalAddGroup_fLT TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT NumberField.AdeleRing.locallyCompactSpace ContinuousLinearEquiv.toContinuousAddEquiv TensorProduct.RightActions.instModule_fLT TensorProduct.RightActions.ContinuousLinearEquiv.baseChange	—	TensorProduct.RightActions.instIsTopologicalAddGroup_fLT TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT NumberField.AdeleRing.locallyCompactSpace addEquivAddHaarChar_eq_addEquivAddHaarChar_of_continuousAddEquiv addHaarScalarFactor_tensor_adeles_rat_eq_one
addHaarScalarFactor_tensor_adeles_rat_eq_one 📖	mathematical	—	NumberField.AdeleRing.instAlgebraRingOfIntegers_fLT TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT TensorProduct.RightActions.instIsTopologicalAddGroup_fLT TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT NumberField.AdeleRing.locallyCompactSpace ContinuousLinearEquiv.toContinuousAddEquiv TensorProduct.RightActions.instModule_fLT TensorProduct.RightActions.ContinuousLinearEquiv.baseChange	—	TensorProduct.RightActions.instIsTopologicalAddGroup_fLT TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT NumberField.AdeleRing.locallyCompactSpace instBorelSpaceAdeleRingRingOfIntegers_fLT addEquivAddHaarChar_eq_ringHaarChar_det_of_existsListTransvecEtc TensorProduct.RightActions.instIsModuleTopology_fLT instSecondCountableTopologyAdeleRingRingOfIntegers_fLT Matrix.Pivot.baseChange_existsListTransvecEtc Matrix.Pivot.exists_list_transvec_mul_diagonal_mul_list_transvec' Matrix.Pivot.ExistsListTransvecMulDiagonalMulListTransvec.congr_simp ringHaarChar_adeles_units_rat_eq_one
ringHaarChar_adeles_rat 📖	mathematical	—	ringHaarChar NumberField.AdeleRing.locallyCompactSpace instMeasurableSpaceAdeleRingRingOfIntegers_fLT instBorelSpaceAdeleRingRingOfIntegers_fLT instMeasurableSpaceInfiniteAdeleRing_fLT instBorelSpaceInfiniteAdeleRing_fLT Rat.adicCompletion.locallyCompactSpace instMeasurableSpaceAdicCompletionRingOfIntegers_fLT instBorelSpaceAdicCompletionRingOfIntegers_fLT MulEquiv.restrictedProductUnits	—	NumberField.AdeleRing.locallyCompactSpace instBorelSpaceAdeleRingRingOfIntegers_fLT instBorelSpaceInfiniteAdeleRing_fLT Rat.adicCompletion.locallyCompactSpace instBorelSpaceAdicCompletionRingOfIntegers_fLT instLocallyCompactSpaceFiniteAdeleRingRingOfIntegers_fLT instBorelSpaceFiniteAdeleRingRingOfIntegers_fLT instSecondCountableTopologyFiniteAdeleRingRingOfIntegers_fLT ringHaarChar_prod' NumberField.isOpenAdicCompletionIntegers NumberField.instCompactSpaceAdicCompletionIntegers instBorelSpaceRestrictedProduct_fLT addEquivAddHaarChar_restrictedProductCongrRight IsDedekindDomain.HeightOneSpectrum.instSeparableSpaceAdicCompletionOfCountable_fLT instCountableOfNumberField_fLT instWeaklyLocallyCompactSpaceAdicCompletionRingOfIntegers_fLT instCountableHeightOneSpectrumRingOfIntegersRat_fLT
ringHaarChar_adeles_units_rat_eq_one 📖	mathematical	—	ringHaarChar NumberField.AdeleRing.locallyCompactSpace instMeasurableSpaceAdeleRingRingOfIntegers_fLT instBorelSpaceAdeleRingRingOfIntegers_fLT NumberField.AdeleRing.instAlgebraRingOfIntegers_fLT	—	NumberField.AdeleRing.locallyCompactSpace instBorelSpaceAdeleRingRingOfIntegers_fLT instBorelSpaceInfiniteAdeleRing_fLT Rat.adicCompletion.locallyCompactSpace instBorelSpaceAdicCompletionRingOfIntegers_fLT ringHaarChar_adeles_rat instBorelSpaceCompletion_fLT instSecondCountableTopologyCompletion_fLT ringHaarChar_pi' ringHaarChar_eq_ringHaarChar_of_continuousAlgEquiv ringHaarChar_real Padic.instBorelSpace ringHaarChar_padic Rat.HeightOneSpectrum.adicCompletion.padicEquiv_norm_eq

NumberField.AdeleRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addEquivAddHaarChar_mulRight_unit_eq_one 📖	mathematical	—	instAlgebraRingOfIntegers_fLT TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT TensorProduct.RightActions.instIsTopologicalAddGroup_fLT TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT locallyCompactSpace ContinuousAddEquiv.mulRight TensorProduct.RightActions.instIsTopologicalRing_fLT_1	—	TensorProduct.RightActions.instIsTopologicalAddGroup_fLT TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT locallyCompactSpace TensorProduct.RightActions.instIsTopologicalRing_fLT_1 MeasureTheory.addHaarScalarFactor_tensor_adeles_eq_one
units_mem_ringHaarCharacter_ker 📖	mathematical	—	instAlgebraRingOfIntegers_fLT MeasureTheory.ringHaarChar_ker TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT TensorProduct.RightActions.instIsTopologicalRing_fLT_1 TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT locallyCompactSpace	—	TensorProduct.RightActions.instIsTopologicalRing_fLT_1 TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT locallyCompactSpace MeasureTheory.mem_ringHaarChar_ker MeasureTheory.ringHaarChar_apply TensorProduct.RightActions.instIsTopologicalAddGroup_fLT MeasureTheory.addHaarScalarFactor_tensor_adeles_eq_one

TensorProduct.RightActions.ContinuousLinearEquiv

Definitions

Name	Category	Theorems
baseChange 📖	CompOp	3 math math: MeasureTheory.addHaarScalarFactor_tensor_adeles_eq_one, ContinuousLinearEquiv.baseChange_apply, MeasureTheory.addHaarScalarFactor_tensor_adeles_rat_eq_one

---

← Back to Index