FiniteAdeleRing

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

Statistics

Metric	Count
Definitions `e`, `f`, `g`, `commContinuousAddMonoidHom`, `commLinearMap`, `b_global`, `b_local`, `instDecidableEqHeightOneSpectrumRingOfIntegers_fLT`, `instMeasurableSpaceTensorProductAdicCompletionRingOfIntegers_fLT`, `instMeasurableSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT`, `instTopologicalSpaceTensorProductAdicCompletionRingOfIntegers_fLT`, `instTopologicalSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT`, `φ_local_Kv_linear`	13
Theorems `almost_always_bijOn`, `almost_always_mapsTo`, `e_commSq`, `f_commSq`, `f_g_local_global`, `g_commSq`, `isCentralSimple_addHaarScalarFactor_left_mul_eq_right_mul`, `tensor_isCentralSimple_addHaarScalarFactor_left_mul_eq_right_mul`, `basis_eq`, `basis_eq_global`, `basis_eq_single`, `basis_eq_single_global`, `basis_repr_eq`, `basis_repr_eq_global`, `instBorelSpaceTensorProductAdicCompletionRingOfIntegers_fLT`, `instBorelSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT`, `instCompactSpaceSubtypeForallChooseBasisIndexAdicCompletionRingOfIntegersMemAddSubgroupPiUnivToAddSubgroupAdicCompletionIntegers_fLT`, `instFactForallIsOpenAdicCompletionRingOfIntegersCoeAddSubgroupToAddSubgroupAdicCompletionIntegers_fLT`, `instFactForallIsOpenForallAdicCompletionRingOfIntegersCoeAddSubgroupPiUnivToAddSubgroupAdicCompletionIntegersOfFinite_fLT`, `instIsCentralTensorProduct_fLT_1`, `instIsModuleTopologyAdicCompletionRingOfIntegersTensorProduct_fLT`, `instIsModuleTopologyFiniteAdeleRingRingOfIntegersTensorProduct_fLT`, `instIsTopologicalAddGroupTensorProductAdicCompletionRingOfIntegers_fLT`, `instIsTopologicalRingTensorProductAdicCompletionRingOfIntegers_fLT`, `instIsTopologicalRingTensorProductFiniteAdeleRingRingOfIntegers_fLT`, `instLocallyCompactSpaceRestrictedProductHeightOneSpectrumRingOfIntegersAdicCompletionCoeAddSubgroupToAddSubgroupAdicCompletionIntegersCofinite_fLT`, `instLocallyCompactSpaceRestrictedProductHeightOneSpectrumRingOfIntegersForallAdicCompletionCoeAddSubgroupPiUnivToAddSubgroupAdicCompletionIntegersCofinite_fLT`, `instLocallyCompactSpaceTensorProductAdicCompletionRingOfIntegers_fLT`, `instLocallyCompactSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT`, `instSecondCountableTopologyRestrictedProductHeightOneSpectrumRingOfIntegersAdicCompletionCoeValuationSubringAdicCompletionIntegersCofinite_fLT`, `localcomponent_matrix`, `localcomponent_mulLeft`, `localcomponent_mulRight`, `toMatrix_f`	34
Total	47

FiniteAdeleRing.Aux

Definitions

Name	Category	Theorems
`e` 📖	CompOp	2 math math: `f_g_local_global`, `e_commSq`
`f` 📖	CompOp	3 math math: `toMatrix_f`, `f_commSq`, `f_g_local_global`
`g` 📖	CompOp	2 math math: `g_commSq`, `f_g_local_global`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`almost_always_bijOn` 📖	—	—	—	—	`instIsTopologicalRingTensorProductFiniteAdeleRingRingOfIntegers_fLT` `instIsModuleTopologyFiniteAdeleRingRingOfIntegersTensorProduct_fLT` `instIsTopologicalAddGroupTensorProductAdicCompletionRingOfIntegers_fLT` `instIsModuleTopologyAdicCompletionRingOfIntegersTensorProduct_fLT` `almost_always_mapsTo`
`almost_always_mapsTo` 📖	—	—	—	—	`instIsTopologicalRingTensorProductFiniteAdeleRingRingOfIntegers_fLT` `instIsModuleTopologyFiniteAdeleRingRingOfIntegersTensorProduct_fLT` `instIsTopologicalAddGroupTensorProductAdicCompletionRingOfIntegers_fLT` `instIsModuleTopologyAdicCompletionRingOfIntegersTensorProduct_fLT` `basis_repr_eq` `localcomponent_matrix` `basis_eq`
`e_commSq` 📖	mathematical	—	`instAlgebraWithVal_fLT_1` `instTopologicalSpaceTensorProductAdicCompletionRingOfIntegers_fLT` `instMeasurableSpaceTensorProductAdicCompletionRingOfIntegers_fLT` `instBorelSpaceTensorProductAdicCompletionRingOfIntegers_fLT` `instIsTopologicalAddGroupTensorProductAdicCompletionRingOfIntegers_fLT` `instLocallyCompactSpaceTensorProductAdicCompletionRingOfIntegers_fLT` `ContinuousLinearEquiv.toContinuousAddEquiv` `instMeasurableSpaceAdicCompletionRingOfIntegers_fLT` `IsDedekindDomain.HeightOneSpectrum.instSeparableSpaceAdicCompletionOfCountable_fLT` `instCountableOfNumberField_fLT` `instBorelSpaceAdicCompletionRingOfIntegers_fLT` `instLocallyCompactSpaceAdicCompletionRingOfIntegers_fLT` `e`	—	`MeasureTheory.addEquivAddHaarChar_eq_addEquivAddHaarChar_of_continuousAddEquiv` `instIsTopologicalAddGroupTensorProductAdicCompletionRingOfIntegers_fLT` `instLocallyCompactSpaceTensorProductAdicCompletionRingOfIntegers_fLT` `instBorelSpaceTensorProductAdicCompletionRingOfIntegers_fLT` `instLocallyCompactSpaceAdicCompletionRingOfIntegers_fLT` `IsDedekindDomain.HeightOneSpectrum.instSeparableSpaceAdicCompletionOfCountable_fLT` `instCountableOfNumberField_fLT` `instBorelSpaceAdicCompletionRingOfIntegers_fLT` `instIsModuleTopologyAdicCompletionRingOfIntegersTensorProduct_fLT`
`f_commSq` 📖	mathematical	—	`IsDedekindDomain.baseChangeAlgebra` `instTopologicalSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT` `instMeasurableSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT` `instBorelSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT` `instIsTopologicalRingTensorProductFiniteAdeleRingRingOfIntegers_fLT` `instLocallyCompactSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT` `ContinuousLinearEquiv.toContinuousAddEquiv` `instMeasurableSpaceFiniteAdeleRingRingOfIntegers_fLT` `instSecondCountableTopologyFiniteAdeleRingRingOfIntegers_fLT` `instBorelSpaceFiniteAdeleRingRingOfIntegers_fLT` `instLocallyCompactSpaceFiniteAdeleRingRingOfIntegers_fLT` `f`	—	`MeasureTheory.addEquivAddHaarChar_eq_addEquivAddHaarChar_of_continuousAddEquiv` `instIsTopologicalRingTensorProductFiniteAdeleRingRingOfIntegers_fLT` `instLocallyCompactSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT` `instBorelSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT` `instLocallyCompactSpaceFiniteAdeleRingRingOfIntegers_fLT` `instSecondCountableTopologyFiniteAdeleRingRingOfIntegers_fLT` `instBorelSpaceFiniteAdeleRingRingOfIntegers_fLT` `instIsModuleTopologyFiniteAdeleRingRingOfIntegersTensorProduct_fLT`
`f_g_local_global` 📖	mathematical	—	`g` `f` `ContinuousAddEquiv.restrictedProductCongrRight` `e` `IsDedekindDomain.FiniteAdeleRing.TensorProduct.localcomponentEquiv` `instDecidableEqHeightOneSpectrumRingOfIntegers_fLT` `instTopologicalSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT` `IsDedekindDomain.baseChangeAlgebra` `instIsTopologicalRingTensorProductFiniteAdeleRingRingOfIntegers_fLT` `instIsModuleTopologyFiniteAdeleRingRingOfIntegersTensorProduct_fLT` `instTopologicalSpaceTensorProductAdicCompletionRingOfIntegers_fLT` `instIsTopologicalAddGroupTensorProductAdicCompletionRingOfIntegers_fLT` `instIsModuleTopologyAdicCompletionRingOfIntegersTensorProduct_fLT` `almost_always_bijOn`	—	`instIsTopologicalRingTensorProductFiniteAdeleRingRingOfIntegers_fLT` `instIsModuleTopologyFiniteAdeleRingRingOfIntegersTensorProduct_fLT` `instIsTopologicalAddGroupTensorProductAdicCompletionRingOfIntegers_fLT` `instIsModuleTopologyAdicCompletionRingOfIntegersTensorProduct_fLT` `almost_always_bijOn` `basis_eq` `basis_repr_eq` `localcomponent_matrix` `toMatrix_f` `NumberField.isOpenAdicCompletionIntegers`
`g_commSq` 📖	mathematical	—	`instMeasurableSpaceFiniteAdeleRingRingOfIntegers_fLT` `instSecondCountableTopologyFiniteAdeleRingRingOfIntegers_fLT` `instBorelSpaceFiniteAdeleRingRingOfIntegers_fLT` `instLocallyCompactSpaceFiniteAdeleRingRingOfIntegers_fLT` `ContinuousLinearEquiv.toContinuousAddEquiv` `instMeasurableSpaceRestrictedProduct_fLT` `instBorelSpaceRestrictedProduct_fLT` `instFactForallIsOpenForallAdicCompletionRingOfIntegersCoeAddSubgroupPiUnivToAddSubgroupAdicCompletionIntegersOfFinite_fLT` `instLocallyCompactSpaceRestrictedProductHeightOneSpectrumRingOfIntegersForallAdicCompletionCoeAddSubgroupPiUnivToAddSubgroupAdicCompletionIntegersCofinite_fLT` `g`	—	`instBorelSpaceRestrictedProduct_fLT` `instFactForallIsOpenForallAdicCompletionRingOfIntegersCoeAddSubgroupPiUnivToAddSubgroupAdicCompletionIntegersOfFinite_fLT` `instLocallyCompactSpaceRestrictedProductHeightOneSpectrumRingOfIntegersForallAdicCompletionCoeAddSubgroupPiUnivToAddSubgroupAdicCompletionIntegersCofinite_fLT` `instSecondCountableTopologyFiniteAdeleRingRingOfIntegers_fLT` `instBorelSpaceFiniteAdeleRingRingOfIntegers_fLT` `instLocallyCompactSpaceFiniteAdeleRingRingOfIntegers_fLT` `NumberField.isOpenAdicCompletionIntegers` `MeasureTheory.addEquivAddHaarChar_eq_addEquivAddHaarChar_of_continuousAddEquiv` `instFactForallIsOpenAdicCompletionRingOfIntegersCoeAddSubgroupToAddSubgroupAdicCompletionIntegers_fLT` `instLocallyCompactSpaceRestrictedProductHeightOneSpectrumRingOfIntegersAdicCompletionCoeAddSubgroupToAddSubgroupAdicCompletionIntegersCofinite_fLT` `instSecondCountableTopologyRestrictedProductHeightOneSpectrumRingOfIntegersAdicCompletionCoeValuationSubringAdicCompletionIntegersCofinite_fLT`

FiniteAdeleRing.TensorProduct

Definitions

Name	Category	Theorems
`commContinuousAddMonoidHom` 📖	CompOp	—
`commLinearMap` 📖	CompOp	—

NumberField.FiniteAdeleRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCentralSimple_addHaarScalarFactor_left_mul_eq_right_mul` 📖	mathematical	—	`IsDedekindDomain.baseChangeAlgebra` `TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT` `TensorProduct.RightActions.instIsTopologicalAddGroup_fLT` `TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT` `instLocallyCompactSpaceFiniteAdeleRingRingOfIntegers_fLT` `ContinuousAddEquiv.mulLeft` `TensorProduct.RightActions.instIsTopologicalRing_fLT_1` `ContinuousAddEquiv.mulRight`	—	`TensorProduct.RightActions.instIsTopologicalAddGroup_fLT` `TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT` `instLocallyCompactSpaceFiniteAdeleRingRingOfIntegers_fLT` `TensorProduct.RightActions.instIsTopologicalRing_fLT_1` `instBorelSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT` `instIsTopologicalRingTensorProductFiniteAdeleRingRingOfIntegers_fLT` `instLocallyCompactSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT` `MeasureTheory.addEquivAddHaarChar_eq_addEquivAddHaarChar_of_continuousAddEquiv` `tensor_isCentralSimple_addHaarScalarFactor_left_mul_eq_right_mul`
`tensor_isCentralSimple_addHaarScalarFactor_left_mul_eq_right_mul` 📖	mathematical	—	`IsDedekindDomain.baseChangeAlgebra` `instTopologicalSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT` `instMeasurableSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT` `instBorelSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT` `instIsTopologicalRingTensorProductFiniteAdeleRingRingOfIntegers_fLT` `instLocallyCompactSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT` `ContinuousAddEquiv.mulLeft` `ContinuousAddEquiv.mulRight`	—	`instBorelSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT` `instIsTopologicalRingTensorProductFiniteAdeleRingRingOfIntegers_fLT` `instLocallyCompactSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT` `instSecondCountableTopologyFiniteAdeleRingRingOfIntegers_fLT` `instBorelSpaceFiniteAdeleRingRingOfIntegers_fLT` `instLocallyCompactSpaceFiniteAdeleRingRingOfIntegers_fLT` `FiniteAdeleRing.Aux.f_commSq` `instBorelSpaceRestrictedProduct_fLT` `instFactForallIsOpenForallAdicCompletionRingOfIntegersCoeAddSubgroupPiUnivToAddSubgroupAdicCompletionIntegersOfFinite_fLT` `instLocallyCompactSpaceRestrictedProductHeightOneSpectrumRingOfIntegersForallAdicCompletionCoeAddSubgroupPiUnivToAddSubgroupAdicCompletionIntegersCofinite_fLT` `FiniteAdeleRing.Aux.g_commSq` `instIsModuleTopologyFiniteAdeleRingRingOfIntegersTensorProduct_fLT` `instIsTopologicalAddGroupTensorProductAdicCompletionRingOfIntegers_fLT` `instIsModuleTopologyAdicCompletionRingOfIntegersTensorProduct_fLT` `FiniteAdeleRing.Aux.almost_always_bijOn` `FiniteAdeleRing.Aux.f_g_local_global` `IsDedekindDomain.HeightOneSpectrum.instSeparableSpaceAdicCompletionOfCountable_fLT` `instCountableOfNumberField_fLT` `instBorelSpaceAdicCompletionRingOfIntegers_fLT` `instLocallyCompactSpaceAdicCompletionRingOfIntegers_fLT` `instCompactSpaceSubtypeForallChooseBasisIndexAdicCompletionRingOfIntegersMemAddSubgroupPiUnivToAddSubgroupAdicCompletionIntegers_fLT` `MeasureTheory.addEquivAddHaarChar_restrictedProductCongrRight` `instWeaklyLocallyCompactSpaceAdicCompletionRingOfIntegers_fLT` `instCountableHeightOneSpectrumRingOfIntegers_fLT` `instBorelSpaceTensorProductAdicCompletionRingOfIntegers_fLT` `instLocallyCompactSpaceTensorProductAdicCompletionRingOfIntegers_fLT` `FiniteAdeleRing.Aux.e_commSq` `instIsTopologicalRingTensorProductAdicCompletionRingOfIntegers_fLT` `IsDedekindDomain.instIsScalarTowerFiniteAdeleRing_fLT` `instIsScalarTowerWithVal_fLT_1` `localcomponent_mulLeft` `localcomponent_mulRight` `IsSimpleRing.ringHaarChar_eq_addEquivAddHaarChar_mulRight` `instIsSimpleRingTensorProductOfIsCentral_fLT_1` `instIsCentralTensorProduct_fLT`

(root)

Definitions

Name	Category	Theorems
`b_global` 📖	CompOp	4 math math: `toMatrix_f`, `basis_eq_single_global`, `basis_repr_eq_global`, `basis_eq_global`
`b_local` 📖	CompOp	3 math math: `basis_repr_eq`, `basis_eq`, `basis_eq_single`
`instDecidableEqHeightOneSpectrumRingOfIntegers_fLT` 📖	CompOp	3 math math: `localcomponent_mulLeft`, `localcomponent_mulRight`, `FiniteAdeleRing.Aux.f_g_local_global`
`instMeasurableSpaceTensorProductAdicCompletionRingOfIntegers_fLT` 📖	CompOp	2 math math: `instBorelSpaceTensorProductAdicCompletionRingOfIntegers_fLT`, `FiniteAdeleRing.Aux.e_commSq`
`instMeasurableSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT` 📖	CompOp	3 math math: `instBorelSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT`, `NumberField.FiniteAdeleRing.tensor_isCentralSimple_addHaarScalarFactor_left_mul_eq_right_mul`, `FiniteAdeleRing.Aux.f_commSq`
`instTopologicalSpaceTensorProductAdicCompletionRingOfIntegers_fLT` 📖	CompOp	12 math math: `basis_repr_eq`, `localcomponent_mulLeft`, `instBorelSpaceTensorProductAdicCompletionRingOfIntegers_fLT`, `localcomponent_mulRight`, `basis_eq`, `instIsTopologicalAddGroupTensorProductAdicCompletionRingOfIntegers_fLT`, `instIsModuleTopologyAdicCompletionRingOfIntegersTensorProduct_fLT`, `basis_eq_single`, `FiniteAdeleRing.Aux.f_g_local_global`, `instIsTopologicalRingTensorProductAdicCompletionRingOfIntegers_fLT`, `instLocallyCompactSpaceTensorProductAdicCompletionRingOfIntegers_fLT`, `FiniteAdeleRing.Aux.e_commSq`
`instTopologicalSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT` 📖	CompOp	14 math math: `toMatrix_f`, `instLocallyCompactSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT`, `localcomponent_mulLeft`, `instBorelSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT`, `basis_eq_single_global`, `localcomponent_mulRight`, `NumberField.FiniteAdeleRing.tensor_isCentralSimple_addHaarScalarFactor_left_mul_eq_right_mul`, `instIsTopologicalRingTensorProductFiniteAdeleRingRingOfIntegers_fLT`, `basis_repr_eq_global`, `FiniteAdeleRing.Aux.f_commSq`, `localcomponent_matrix`, `FiniteAdeleRing.Aux.f_g_local_global`, `basis_eq_global`, `instIsModuleTopologyFiniteAdeleRingRingOfIntegersTensorProduct_fLT`
`φ_local_Kv_linear` 📖	CompOp	1 math math: `localcomponent_matrix`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`basis_eq` 📖	mathematical	—	`b_local` `instTopologicalSpaceTensorProductAdicCompletionRingOfIntegers_fLT` `ContinuousLinearEquiv.toContinuousAddEquiv` `ContinuousLinearEquiv.chooseBasis_piScalarRight'` `instIsTopologicalAddGroupTensorProductAdicCompletionRingOfIntegers_fLT` `instIsModuleTopologyAdicCompletionRingOfIntegersTensorProduct_fLT`	—	`instIsTopologicalAddGroupTensorProductAdicCompletionRingOfIntegers_fLT` `instIsModuleTopologyAdicCompletionRingOfIntegersTensorProduct_fLT` `basis_eq_single`
`basis_eq_global` 📖	mathematical	—	`IsDedekindDomain.baseChangeAlgebra` `b_global` `instTopologicalSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT` `ContinuousLinearEquiv.toContinuousAddEquiv` `ContinuousLinearEquiv.chooseBasis_piScalarRight'` `instIsTopologicalRingTensorProductFiniteAdeleRingRingOfIntegers_fLT` `instIsModuleTopologyFiniteAdeleRingRingOfIntegersTensorProduct_fLT`	—	`instIsTopologicalRingTensorProductFiniteAdeleRingRingOfIntegers_fLT` `instIsModuleTopologyFiniteAdeleRingRingOfIntegersTensorProduct_fLT` `basis_eq_single_global`
`basis_eq_single` 📖	mathematical	—	`b_local` `instTopologicalSpaceTensorProductAdicCompletionRingOfIntegers_fLT` `ContinuousLinearEquiv.chooseBasis_piScalarRight'` `instIsTopologicalAddGroupTensorProductAdicCompletionRingOfIntegers_fLT` `instIsModuleTopologyAdicCompletionRingOfIntegersTensorProduct_fLT`	—	`instIsTopologicalAddGroupTensorProductAdicCompletionRingOfIntegers_fLT` `instIsModuleTopologyAdicCompletionRingOfIntegersTensorProduct_fLT`
`basis_eq_single_global` 📖	mathematical	—	`IsDedekindDomain.baseChangeAlgebra` `b_global` `instTopologicalSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT` `ContinuousLinearEquiv.chooseBasis_piScalarRight'` `instIsTopologicalRingTensorProductFiniteAdeleRingRingOfIntegers_fLT` `instIsModuleTopologyFiniteAdeleRingRingOfIntegersTensorProduct_fLT`	—	`instIsTopologicalRingTensorProductFiniteAdeleRingRingOfIntegers_fLT` `instIsModuleTopologyFiniteAdeleRingRingOfIntegersTensorProduct_fLT`
`basis_repr_eq` 📖	mathematical	—	`b_local` `instTopologicalSpaceTensorProductAdicCompletionRingOfIntegers_fLT` `ContinuousLinearEquiv.chooseBasis_piScalarRight'` `instIsTopologicalAddGroupTensorProductAdicCompletionRingOfIntegers_fLT` `instIsModuleTopologyAdicCompletionRingOfIntegersTensorProduct_fLT`	—	`instIsTopologicalAddGroupTensorProductAdicCompletionRingOfIntegers_fLT` `instIsModuleTopologyAdicCompletionRingOfIntegersTensorProduct_fLT`
`basis_repr_eq_global` 📖	mathematical	—	`IsDedekindDomain.baseChangeAlgebra` `b_global` `instTopologicalSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT` `ContinuousLinearEquiv.chooseBasis_piScalarRight'` `instIsTopologicalRingTensorProductFiniteAdeleRingRingOfIntegers_fLT` `instIsModuleTopologyFiniteAdeleRingRingOfIntegersTensorProduct_fLT`	—	`instIsTopologicalRingTensorProductFiniteAdeleRingRingOfIntegers_fLT` `instIsModuleTopologyFiniteAdeleRingRingOfIntegersTensorProduct_fLT`
`instBorelSpaceTensorProductAdicCompletionRingOfIntegers_fLT` 📖	mathematical	—	`instAlgebraWithVal_fLT_1` `instTopologicalSpaceTensorProductAdicCompletionRingOfIntegers_fLT` `instMeasurableSpaceTensorProductAdicCompletionRingOfIntegers_fLT`	—	—
`instBorelSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT` 📖	mathematical	—	`IsDedekindDomain.baseChangeAlgebra` `instTopologicalSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT` `instMeasurableSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT`	—	—
`instCompactSpaceSubtypeForallChooseBasisIndexAdicCompletionRingOfIntegersMemAddSubgroupPiUnivToAddSubgroupAdicCompletionIntegers_fLT` 📖	—	—	—	—	`NumberField.isCompactAdicCompletionIntegers`
`instFactForallIsOpenAdicCompletionRingOfIntegersCoeAddSubgroupToAddSubgroupAdicCompletionIntegers_fLT` 📖	—	—	—	—	`NumberField.isOpenAdicCompletionIntegers`
`instFactForallIsOpenForallAdicCompletionRingOfIntegersCoeAddSubgroupPiUnivToAddSubgroupAdicCompletionIntegersOfFinite_fLT` 📖	—	—	—	—	`NumberField.isOpenAdicCompletionIntegers`
`instIsCentralTensorProduct_fLT_1` 📖	mathematical	—	`TensorProduct.RightActions.instAlgebra_fLT`	—	`instIsCentralTensorProduct_fLT`
`instIsModuleTopologyAdicCompletionRingOfIntegersTensorProduct_fLT` 📖	mathematical	—	`instAlgebraWithVal_fLT_1` `instTopologicalSpaceTensorProductAdicCompletionRingOfIntegers_fLT`	—	—
`instIsModuleTopologyFiniteAdeleRingRingOfIntegersTensorProduct_fLT` 📖	mathematical	—	`IsDedekindDomain.baseChangeAlgebra` `instTopologicalSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT`	—	—
`instIsTopologicalAddGroupTensorProductAdicCompletionRingOfIntegers_fLT` 📖	mathematical	—	`instAlgebraWithVal_fLT_1` `instTopologicalSpaceTensorProductAdicCompletionRingOfIntegers_fLT`	—	`instIsModuleTopologyAdicCompletionRingOfIntegersTensorProduct_fLT`
`instIsTopologicalRingTensorProductAdicCompletionRingOfIntegers_fLT` 📖	mathematical	—	`instAlgebraWithVal_fLT_1` `instTopologicalSpaceTensorProductAdicCompletionRingOfIntegers_fLT`	—	`instIsModuleTopologyAdicCompletionRingOfIntegersTensorProduct_fLT`
`instIsTopologicalRingTensorProductFiniteAdeleRingRingOfIntegers_fLT` 📖	mathematical	—	`IsDedekindDomain.baseChangeAlgebra` `instTopologicalSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT`	—	`instIsModuleTopologyFiniteAdeleRingRingOfIntegersTensorProduct_fLT`
`instLocallyCompactSpaceRestrictedProductHeightOneSpectrumRingOfIntegersAdicCompletionCoeAddSubgroupToAddSubgroupAdicCompletionIntegersCofinite_fLT` 📖	—	—	—	—	`instFactForallIsOpenAdicCompletionRingOfIntegersCoeAddSubgroupToAddSubgroupAdicCompletionIntegers_fLT` `instLocallyCompactSpaceAdicCompletionRingOfIntegers_fLT` `NumberField.isCompactAdicCompletionIntegers`
`instLocallyCompactSpaceRestrictedProductHeightOneSpectrumRingOfIntegersForallAdicCompletionCoeAddSubgroupPiUnivToAddSubgroupAdicCompletionIntegersCofinite_fLT` 📖	—	—	—	—	`instFactForallIsOpenForallAdicCompletionRingOfIntegersCoeAddSubgroupPiUnivToAddSubgroupAdicCompletionIntegersOfFinite_fLT` `instLocallyCompactSpaceAdicCompletionRingOfIntegers_fLT` `NumberField.isCompactAdicCompletionIntegers`
`instLocallyCompactSpaceTensorProductAdicCompletionRingOfIntegers_fLT` 📖	mathematical	—	`instAlgebraWithVal_fLT_1` `instTopologicalSpaceTensorProductAdicCompletionRingOfIntegers_fLT`	—	`IsModuleTopology.locallyCompactSpaceOfFinite` `instIsModuleTopologyAdicCompletionRingOfIntegersTensorProduct_fLT` `instLocallyCompactSpaceAdicCompletionRingOfIntegers_fLT`
`instLocallyCompactSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT` 📖	mathematical	—	`IsDedekindDomain.baseChangeAlgebra` `instTopologicalSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT`	—	`IsModuleTopology.locallyCompactSpaceOfFinite` `instIsModuleTopologyFiniteAdeleRingRingOfIntegersTensorProduct_fLT` `instLocallyCompactSpaceFiniteAdeleRingRingOfIntegers_fLT`
`instSecondCountableTopologyRestrictedProductHeightOneSpectrumRingOfIntegersAdicCompletionCoeValuationSubringAdicCompletionIntegersCofinite_fLT` 📖	—	—	—	—	`instSecondCountableTopologyFiniteAdeleRingRingOfIntegers_fLT`
`localcomponent_matrix` 📖	mathematical	—	`φ_local_Kv_linear` `IsDedekindDomain.baseChangeAlgebra` `instTopologicalSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT`	—	`AlgHom.rTensor_map_smul` `IsDedekindDomain.FiniteAdeleRing.evalAlgebraMap_singleLinearMap`
`localcomponent_mulLeft` 📖	mathematical	—	`ContinuousLinearEquiv.toContinuousAddEquiv` `instTopologicalSpaceTensorProductAdicCompletionRingOfIntegers_fLT` `IsDedekindDomain.FiniteAdeleRing.TensorProduct.localcomponentEquiv` `instDecidableEqHeightOneSpectrumRingOfIntegers_fLT` `instTopologicalSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT` `IsDedekindDomain.baseChangeAlgebra` `instIsTopologicalRingTensorProductFiniteAdeleRingRingOfIntegers_fLT` `instIsModuleTopologyFiniteAdeleRingRingOfIntegersTensorProduct_fLT` `instIsTopologicalAddGroupTensorProductAdicCompletionRingOfIntegers_fLT` `instIsModuleTopologyAdicCompletionRingOfIntegersTensorProduct_fLT` `ContinuousLinearEquiv.mulLeft` `ContinuousAddEquiv.mulLeft` `instIsTopologicalRingTensorProductAdicCompletionRingOfIntegers_fLT` `IsDedekindDomain.instIsScalarTowerFiniteAdeleRing_fLT` `instIsScalarTowerWithVal_fLT_1` `IsDedekindDomain.FiniteAdeleRing.evalContinuousAlgebraMap`	—	`instIsTopologicalRingTensorProductFiniteAdeleRingRingOfIntegers_fLT` `instIsModuleTopologyFiniteAdeleRingRingOfIntegersTensorProduct_fLT` `instIsTopologicalAddGroupTensorProductAdicCompletionRingOfIntegers_fLT` `instIsModuleTopologyAdicCompletionRingOfIntegersTensorProduct_fLT` `instIsTopologicalRingTensorProductAdicCompletionRingOfIntegers_fLT` `IsDedekindDomain.instIsScalarTowerFiniteAdeleRing_fLT` `instIsScalarTowerWithVal_fLT_1` `IsDedekindDomain.FiniteAdeleRing.TensorProduct.localcomponent_apply` `IsDedekindDomain.FiniteAdeleRing.evalContinuousAlgebraMap_singleContinuousLinearMap` `ContinuousLinearMap.rTensor.eq_1`
`localcomponent_mulRight` 📖	mathematical	—	`ContinuousLinearEquiv.toContinuousAddEquiv` `instTopologicalSpaceTensorProductAdicCompletionRingOfIntegers_fLT` `IsDedekindDomain.FiniteAdeleRing.TensorProduct.localcomponentEquiv` `instDecidableEqHeightOneSpectrumRingOfIntegers_fLT` `instTopologicalSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT` `IsDedekindDomain.baseChangeAlgebra` `instIsTopologicalRingTensorProductFiniteAdeleRingRingOfIntegers_fLT` `instIsModuleTopologyFiniteAdeleRingRingOfIntegersTensorProduct_fLT` `instIsTopologicalAddGroupTensorProductAdicCompletionRingOfIntegers_fLT` `instIsModuleTopologyAdicCompletionRingOfIntegersTensorProduct_fLT` `ContinuousLinearEquiv.mulRight` `ContinuousAddEquiv.mulRight` `instIsTopologicalRingTensorProductAdicCompletionRingOfIntegers_fLT` `IsDedekindDomain.instIsScalarTowerFiniteAdeleRing_fLT` `instIsScalarTowerWithVal_fLT_1` `IsDedekindDomain.FiniteAdeleRing.evalContinuousAlgebraMap`	—	`instIsTopologicalRingTensorProductFiniteAdeleRingRingOfIntegers_fLT` `instIsModuleTopologyFiniteAdeleRingRingOfIntegersTensorProduct_fLT` `instIsTopologicalAddGroupTensorProductAdicCompletionRingOfIntegers_fLT` `instIsModuleTopologyAdicCompletionRingOfIntegersTensorProduct_fLT` `instIsTopologicalRingTensorProductAdicCompletionRingOfIntegers_fLT` `IsDedekindDomain.instIsScalarTowerFiniteAdeleRing_fLT` `instIsScalarTowerWithVal_fLT_1` `IsDedekindDomain.FiniteAdeleRing.TensorProduct.localcomponent_apply` `IsDedekindDomain.FiniteAdeleRing.evalContinuousAlgebraMap_singleContinuousLinearMap` `ContinuousLinearMap.rTensor.eq_1`
`toMatrix_f` 📖	mathematical	—	`IsDedekindDomain.baseChangeAlgebra` `b_global` `instTopologicalSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT` `FiniteAdeleRing.Aux.f`	—	`instIsTopologicalRingTensorProductFiniteAdeleRingRingOfIntegers_fLT` `instIsModuleTopologyFiniteAdeleRingRingOfIntegersTensorProduct_fLT` `basis_eq_global` `basis_repr_eq_global`

---

← Back to Index