Finiteness

📁 Source: FLT/DivisionAlgebra/Finiteness.lean

Statistics

Metric	Count
Definitions C, D_iso, Df, Dfx, Dinf, Dinfx, D𝔸_iso, D𝔸_iso_top, D𝔸_prodRight, D𝔸_prodRight', D𝔸_prodRight'', D𝔸_prodRight_units, E, Efamily, M, T, Uf, Ui, X, Y, incl, incl_D𝔸quot, incl_Kn_𝔸Kn, includeLeft_subgroup, incl₁, incl₂, instAlgebraRealDinf, instMeasurableSpaceDf, instMeasurableSpaceDinf, instMeasurableSpaceTensorProductRingOfIntegers_fLT, instModuleRingOfIntegersProdDinfDf, rest₁, toQuot, instMeasurableSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT, instTopologicalSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT, Dinf_tensorPi_equiv_piTensor, Dinf_tensorPi_equiv_piTensor_aux, Dinf_tensorPi_equiv_piTensor_mulEquiv, instAlgebraRealCompletion_fLT, instAlgebraRealTensorProductCompletion_fLT, real_to_completion, termD_𝔸	42
Theorems C_compact, D_discrete, D_discrete_aux, D𝔸_prodRight_units_cont, E_compact, E_family_compact, E_family_nonempty_interior, E_family_unbounded, E_noninjective_left, E_noninjective_right, ImAux_isCompact, Kn_discrete, M_compact, T_finite, T_finite_extracted1, spec, spec, X_compact, X_meets_kernel, X_meets_kernel', Y_compact, antidiag_mem_C, compact_includeLeft_subgroup, discrete_includeLeft_subgroup, discrete_principalSubgroup, existsE, incl_D𝔸quot_continuous, incl_D𝔸quot_equivariant, incl_D𝔸quot_surjective, incl₂_isClosedEmbedding, instBorelSpaceDf, instBorelSpaceDinf, instBorelSpaceTensorProductRingOfIntegers_fLT, instFiniteRealDinf, instIsModuleTopologyRealDinf, instIsModuleTopologyRingOfIntegersProdDinfDf, instIsScalarTowerRealInfiniteAdeleRingDinf, instSecondCountableTopologyDinf, instT2SpaceTensorProductRingOfIntegers_fLT, not_injective_of_large_measure, rest₁_continuous, rest₁_surjective, ringHaarChar_D𝔸, ringHaarChar_D𝔸_prodRight_units_aux, ringHaarChar_D𝔸_real_surjective, smul_D𝔸_prodRight_symm, toQuot_cont, toQuot_surjective, compact_quotient, instBorelSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT, isCentralSimple_addHaarScalarFactor_left_mul_eq_right_mul, finiteDoubleCoset, units_cocompact, algebraMap_completion, algebraMap_completion_def, instContinuousSMulRealCompletion_fLT, instFiniteRealCompletion_fLT, instIsModuleTopologyRealCompletion_fLT, instIsModuleTopologyRealForallTensorProductCompletion_fLT, instIsModuleTopologyRealTensorProductCompletion_fLT, instIsScalarTowerRealCompletionTensorProduct_fLT, instSecondCountableTopologyTensorProductCompletion_fLT, isCentralSimple_infinite_addHaarScalarFactor_left_mul_eq_right_mul, isCentralSimple_infinite_addHaarScalarFactor_left_mul_eq_right_mul_aux, tensorPi_equiv_piTensor_map_mul	65
Total	107

NumberField.AdeleRing

Definitions

Name	Category	Theorems
instMeasurableSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT 📖	CompOp	1 math math: instBorelSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT
instTopologicalSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT 📖	CompOp	1 math math: instBorelSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instBorelSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT 📖	mathematical	—	IsDedekindDomain.baseChangeAlgebra instTopologicalSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT instMeasurableSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT	—	—
isCentralSimple_addHaarScalarFactor_left_mul_eq_right_mul 📖	mathematical	—	instAlgebraRingOfIntegers_fLT TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT DivisionAlgebra.Aux.instMeasurableSpaceTensorProductRingOfIntegers_fLT DivisionAlgebra.Aux.instBorelSpaceTensorProductRingOfIntegers_fLT TensorProduct.RightActions.instIsTopologicalAddGroup_fLT TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT locallyCompactSpace ContinuousAddEquiv.mulLeft TensorProduct.RightActions.instIsTopologicalRing_fLT_1 ContinuousAddEquiv.mulRight	—	DivisionAlgebra.Aux.instBorelSpaceTensorProductRingOfIntegers_fLT TensorProduct.RightActions.instIsTopologicalAddGroup_fLT TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT locallyCompactSpace TensorProduct.RightActions.instIsTopologicalRing_fLT_1 DivisionAlgebra.Aux.instBorelSpaceDinf DivisionAlgebra.Aux.instBorelSpaceDf instLocallyCompactSpaceFiniteAdeleRingRingOfIntegers_fLT DivisionAlgebra.Aux.instSecondCountableTopologyDinf MeasureTheory.addEquivAddHaarChar_prodCongr MeasureTheory.addEquivAddHaarChar_eq_addEquivAddHaarChar_of_continuousAddEquiv NumberField.InfiniteAdeleRing.isCentralSimple_infinite_addHaarScalarFactor_left_mul_eq_right_mul NumberField.FiniteAdeleRing.isCentralSimple_addHaarScalarFactor_left_mul_eq_right_mul

NumberField.AdeleRing.DivisionAlgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compact_quotient 📖	mathematical	—	NumberField.AdeleRing.instAlgebraRingOfIntegers_fLT MeasureTheory.ringHaarChar_ker TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT TensorProduct.RightActions.instIsTopologicalRing_fLT_1 TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT NumberField.AdeleRing.locallyCompactSpace Aux.instMeasurableSpaceTensorProductRingOfIntegers_fLT Aux.instBorelSpaceTensorProductRingOfIntegers_fLT Aux.incl	—	TensorProduct.RightActions.instIsTopologicalRing_fLT_1 TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT NumberField.AdeleRing.locallyCompactSpace Aux.instBorelSpaceTensorProductRingOfIntegers_fLT Aux.toQuot_surjective Aux.M_compact Aux.toQuot_cont

NumberField.AdeleRing.DivisionAlgebra.Aux

Definitions

Name	Category	Theorems
C 📖	CompOp	3 math math: C_compact, ImAux_isCompact, antidiag_mem_C
D_iso 📖	CompOp	1 math math: D_discrete_aux
Df 📖	CompOp	12 math math: incl_D𝔸quot_surjective, incl_D𝔸quot_equivariant, ringHaarChar_D𝔸, incl_D𝔸quot_continuous, smul_D𝔸_prodRight_symm, instBorelSpaceDf, instIsModuleTopologyRingOfIntegersProdDinfDf, D𝔸_prodRight_units_cont, ringHaarChar_D𝔸_prodRight_units_aux, rest₁_continuous, ringHaarChar_D𝔸_real_surjective, NumberField.FiniteAdeleRing.DivisionAlgebra.units_cocompact
Dfx 📖	CompOp	11 math math: incl_D𝔸quot_surjective, incl_D𝔸quot_equivariant, ringHaarChar_D𝔸, incl_D𝔸quot_continuous, smul_D𝔸_prodRight_symm, D𝔸_prodRight_units_cont, ringHaarChar_D𝔸_prodRight_units_aux, rest₁_surjective, rest₁_continuous, ringHaarChar_D𝔸_real_surjective, NumberField.FiniteAdeleRing.DivisionAlgebra.units_cocompact
Dinf 📖	CompOp	13 math math: instIsScalarTowerRealInfiniteAdeleRingDinf, NumberField.InfiniteAdeleRing.tensorPi_equiv_piTensor_map_mul, instIsModuleTopologyRealDinf, ringHaarChar_D𝔸, NumberField.InfiniteAdeleRing.isCentralSimple_infinite_addHaarScalarFactor_left_mul_eq_right_mul, smul_D𝔸_prodRight_symm, instIsModuleTopologyRingOfIntegersProdDinfDf, instFiniteRealDinf, D𝔸_prodRight_units_cont, ringHaarChar_D𝔸_prodRight_units_aux, ringHaarChar_D𝔸_real_surjective, instSecondCountableTopologyDinf, instBorelSpaceDinf
Dinfx 📖	CompOp	5 math math: ringHaarChar_D𝔸, smul_D𝔸_prodRight_symm, D𝔸_prodRight_units_cont, ringHaarChar_D𝔸_prodRight_units_aux, ringHaarChar_D𝔸_real_surjective
D𝔸_iso 📖	CompOp	—
D𝔸_iso_top 📖	CompOp	1 math math: D_discrete_aux
D𝔸_prodRight 📖	CompOp	1 math math: smul_D𝔸_prodRight_symm
D𝔸_prodRight' 📖	CompOp	—
D𝔸_prodRight'' 📖	CompOp	—
D𝔸_prodRight_units 📖	CompOp	5 math math: ringHaarChar_D𝔸, smul_D𝔸_prodRight_symm, D𝔸_prodRight_units_cont, ringHaarChar_D𝔸_prodRight_units_aux, ringHaarChar_D𝔸_real_surjective
E 📖	CompOp	3 math math: E_noninjective_right, E_compact, E_noninjective_left
Efamily 📖	CompOp	3 math math: E_family_compact, E_family_unbounded, E_family_nonempty_interior
M 📖	CompOp	2 math math: toQuot_surjective, M_compact
T 📖	CompOp	1 math math: T_finite
Uf 📖	CompOp	1 math math: Uf.spec
Ui 📖	CompOp	1 math math: Ui.spec
X 📖	CompOp	3 math math: X_compact, X_meets_kernel, X_meets_kernel'
Y 📖	CompOp	2 math math: T_finite_extracted1, Y_compact
incl 📖	CompOp	8 math math: incl_D𝔸quot_surjective, incl_D𝔸quot_continuous, toQuot_cont, toQuot_surjective, X_meets_kernel, NumberField.AdeleRing.DivisionAlgebra.compact_quotient, X_meets_kernel', antidiag_mem_C
incl_D𝔸quot 📖	CompOp	2 math math: incl_D𝔸quot_surjective, incl_D𝔸quot_continuous
incl_Kn_𝔸Kn 📖	CompOp	2 math math: Kn_discrete, D_discrete_aux
includeLeft_subgroup 📖	CompOp	2 math math: compact_includeLeft_subgroup, discrete_includeLeft_subgroup
incl₁ 📖	CompOp	5 math math: incl_D𝔸quot_surjective, incl_D𝔸quot_equivariant, incl_D𝔸quot_continuous, NumberField.FiniteAdeleRing.DivisionAlgebra.finiteDoubleCoset, NumberField.FiniteAdeleRing.DivisionAlgebra.units_cocompact
incl₂ 📖	CompOp	1 math math: incl₂_isClosedEmbedding
instAlgebraRealDinf 📖	CompOp	4 math math: instIsScalarTowerRealInfiniteAdeleRingDinf, instIsModuleTopologyRealDinf, instFiniteRealDinf, ringHaarChar_D𝔸_real_surjective
instMeasurableSpaceDf 📖	CompOp	2 math math: ringHaarChar_D𝔸, instBorelSpaceDf
instMeasurableSpaceDinf 📖	CompOp	3 math math: ringHaarChar_D𝔸, NumberField.InfiniteAdeleRing.isCentralSimple_infinite_addHaarScalarFactor_left_mul_eq_right_mul, instBorelSpaceDinf
instMeasurableSpaceTensorProductRingOfIntegers_fLT 📖	CompOp	15 math math: incl_D𝔸quot_surjective, ringHaarChar_D𝔸, incl_D𝔸quot_continuous, toQuot_cont, instBorelSpaceTensorProductRingOfIntegers_fLT, toQuot_surjective, NumberField.AdeleRing.isCentralSimple_addHaarScalarFactor_left_mul_eq_right_mul, ringHaarChar_D𝔸_prodRight_units_aux, NumberField.AdeleRing.DivisionAlgebra.compact_quotient, rest₁_surjective, rest₁_continuous, ringHaarChar_D𝔸_real_surjective, M_compact, incl₂_isClosedEmbedding, E_family_unbounded
instModuleRingOfIntegersProdDinfDf 📖	CompOp	1 math math: instIsModuleTopologyRingOfIntegersProdDinfDf
rest₁ 📖	CompOp	3 math math: incl_D𝔸quot_equivariant, rest₁_surjective, rest₁_continuous
toQuot 📖	CompOp	2 math math: toQuot_cont, toQuot_surjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
C_compact 📖	mathematical	—	NumberField.AdeleRing.instAlgebraRingOfIntegers_fLT TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT C	—	TensorProduct.RightActions.instIsTopologicalRing_fLT_1 T_finite X_compact
D_discrete 📖	mathematical	—	NumberField.AdeleRing.instAlgebraRingOfIntegers_fLT TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT	—	Discrete_of_HomeoDiscrete Discrete_of_HomDiscrete D_discrete_aux Kn_discrete
D_discrete_aux 📖	mathematical	—	incl_Kn_𝔸Kn D_iso NumberField.AdeleRing.instAlgebraRingOfIntegers_fLT TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT TensorProduct.RightActions.instModule_fLT D𝔸_iso_top	—	—
D𝔸_prodRight_units_cont 📖	mathematical	—	NumberField.AdeleRing.instAlgebraRingOfIntegers_fLT Dinfx Dfx TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT Dinf NumberField.InfiniteAdeleRing.instAlgebra_fLT_1 Df IsDedekindDomain.baseChangeAlgebra D𝔸_prodRight_units	—	TensorProduct.RightActions.instIsModuleTopology_fLT TensorProduct.RightActions.instIsTopologicalRing_fLT_1 instIsModuleTopologyRingOfIntegersProdDinfDf
E_compact 📖	mathematical	—	NumberField.AdeleRing.instAlgebraRingOfIntegers_fLT TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT E	—	instBorelSpaceTensorProductRingOfIntegers_fLT TensorProduct.RightActions.instIsTopologicalAddGroup_fLT TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT NumberField.AdeleRing.locallyCompactSpace existsE
E_family_compact 📖	mathematical	—	NumberField.AdeleRing.instAlgebraRingOfIntegers_fLT TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT Efamily	—	Ui.spec TensorProduct.RightActions.instIsTopologicalRing_fLT_1 Uf.spec
E_family_nonempty_interior 📖	mathematical	—	NumberField.AdeleRing.instAlgebraRingOfIntegers_fLT TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT Efamily	—	Ui.spec Uf.spec
E_family_unbounded 📖	mathematical	—	NumberField.AdeleRing.instAlgebraRingOfIntegers_fLT instMeasurableSpaceTensorProductRingOfIntegers_fLT TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT TensorProduct.RightActions.instIsTopologicalAddGroup_fLT instBorelSpaceTensorProductRingOfIntegers_fLT TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT NumberField.AdeleRing.locallyCompactSpace Efamily	—	TensorProduct.RightActions.instIsTopologicalAddGroup_fLT instBorelSpaceTensorProductRingOfIntegers_fLT TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT NumberField.AdeleRing.locallyCompactSpace TensorProduct.RightActions.instIsTopologicalRing_fLT_1 MeasureTheory.ringHaarChar_mul_volume smul_D𝔸_prodRight_symm E_family_nonempty_interior E_family_compact ringHaarChar_D𝔸_real_surjective
E_noninjective_left 📖	mathematical	NumberField.AdeleRing.instAlgebraRingOfIntegers_fLT MeasureTheory.ringHaarChar_ker TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT TensorProduct.RightActions.instIsTopologicalRing_fLT_1 TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT NumberField.AdeleRing.locallyCompactSpace instMeasurableSpaceTensorProductRingOfIntegers_fLT instBorelSpaceTensorProductRingOfIntegers_fLT	E	—	TensorProduct.RightActions.instIsTopologicalRing_fLT_1 TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT NumberField.AdeleRing.locallyCompactSpace instBorelSpaceTensorProductRingOfIntegers_fLT TensorProduct.RightActions.instIsTopologicalAddGroup_fLT existsE
E_noninjective_right 📖	mathematical	NumberField.AdeleRing.instAlgebraRingOfIntegers_fLT MeasureTheory.ringHaarChar_ker TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT TensorProduct.RightActions.instIsTopologicalRing_fLT_1 TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT NumberField.AdeleRing.locallyCompactSpace instMeasurableSpaceTensorProductRingOfIntegers_fLT instBorelSpaceTensorProductRingOfIntegers_fLT	E	—	TensorProduct.RightActions.instIsTopologicalRing_fLT_1 TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT NumberField.AdeleRing.locallyCompactSpace instBorelSpaceTensorProductRingOfIntegers_fLT TensorProduct.RightActions.instIsTopologicalAddGroup_fLT NumberField.AdeleRing.isCentralSimple_addHaarScalarFactor_left_mul_eq_right_mul MeasureTheory.ringHaarChar_apply MeasureTheory.mem_ringHaarChar_ker existsE
ImAux_isCompact 📖	mathematical	—	NumberField.AdeleRing.instAlgebraRingOfIntegers_fLT TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT C	—	C_compact
Kn_discrete 📖	mathematical	—	incl_Kn_𝔸Kn	—	DiscretePi NumberField.AdeleRing.discrete
M_compact 📖	mathematical	—	NumberField.AdeleRing.instAlgebraRingOfIntegers_fLT MeasureTheory.ringHaarChar_ker TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT TensorProduct.RightActions.instIsTopologicalRing_fLT_1 TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT NumberField.AdeleRing.locallyCompactSpace instMeasurableSpaceTensorProductRingOfIntegers_fLT instBorelSpaceTensorProductRingOfIntegers_fLT M	—	TensorProduct.RightActions.instIsTopologicalRing_fLT_1 TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT NumberField.AdeleRing.locallyCompactSpace instBorelSpaceTensorProductRingOfIntegers_fLT incl₂_isClosedEmbedding ImAux_isCompact
T_finite 📖	mathematical	—	NumberField.AdeleRing.instAlgebraRingOfIntegers_fLT T	—	T_finite_extracted1 inter_Discrete discrete_includeLeft_subgroup
T_finite_extracted1 📖	mathematical	—	NumberField.AdeleRing.instAlgebraRingOfIntegers_fLT TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT Y	—	Y_compact discrete_includeLeft_subgroup TensorProduct.RightActions.instIsTopologicalAddGroup_fLT instT2SpaceTensorProductRingOfIntegers_fLT
X_compact 📖	mathematical	—	NumberField.AdeleRing.instAlgebraRingOfIntegers_fLT TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT X	—	E_compact TensorProduct.RightActions.instIsTopologicalAddGroup_fLT
X_meets_kernel 📖	mathematical	NumberField.AdeleRing.instAlgebraRingOfIntegers_fLT MeasureTheory.ringHaarChar_ker TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT TensorProduct.RightActions.instIsTopologicalRing_fLT_1 TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT NumberField.AdeleRing.locallyCompactSpace instMeasurableSpaceTensorProductRingOfIntegers_fLT instBorelSpaceTensorProductRingOfIntegers_fLT	X incl	—	TensorProduct.RightActions.instIsTopologicalRing_fLT_1 TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT NumberField.AdeleRing.locallyCompactSpace instBorelSpaceTensorProductRingOfIntegers_fLT E_noninjective_left
X_meets_kernel' 📖	mathematical	NumberField.AdeleRing.instAlgebraRingOfIntegers_fLT MeasureTheory.ringHaarChar_ker TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT TensorProduct.RightActions.instIsTopologicalRing_fLT_1 TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT NumberField.AdeleRing.locallyCompactSpace instMeasurableSpaceTensorProductRingOfIntegers_fLT instBorelSpaceTensorProductRingOfIntegers_fLT	X incl	—	TensorProduct.RightActions.instIsTopologicalRing_fLT_1 TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT NumberField.AdeleRing.locallyCompactSpace instBorelSpaceTensorProductRingOfIntegers_fLT E_noninjective_right
Y_compact 📖	mathematical	—	NumberField.AdeleRing.instAlgebraRingOfIntegers_fLT TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT Y	—	X_compact TensorProduct.RightActions.instIsTopologicalRing_fLT_1
antidiag_mem_C 📖	mathematical	NumberField.AdeleRing.instAlgebraRingOfIntegers_fLT MeasureTheory.ringHaarChar_ker TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT TensorProduct.RightActions.instIsTopologicalRing_fLT_1 TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT NumberField.AdeleRing.locallyCompactSpace instMeasurableSpaceTensorProductRingOfIntegers_fLT instBorelSpaceTensorProductRingOfIntegers_fLT	incl C	—	TensorProduct.RightActions.instIsTopologicalRing_fLT_1 TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT NumberField.AdeleRing.locallyCompactSpace instBorelSpaceTensorProductRingOfIntegers_fLT X_meets_kernel X_meets_kernel' NumberField.AdeleRing.units_mem_ringHaarCharacter_ker
compact_includeLeft_subgroup 📖	mathematical	—	NumberField.AdeleRing.instAlgebraRingOfIntegers_fLT includeLeft_subgroup TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT	—	NumberField.AdeleRing.cocompact discrete_principalSubgroup TopologicalAddGroup.IsSES.ofClosedAddSubgroup instT2SpaceAdeleRingRingOfIntegers_fLT TopologicalAddGroup.IsSES.isOpenQuotientMap TensorProduct.RightActions.instIsTopologicalRing_fLT_1 TensorProduct.RightActions.instIsModuleTopology_fLT
discrete_includeLeft_subgroup 📖	mathematical	—	NumberField.AdeleRing.instAlgebraRingOfIntegers_fLT includeLeft_subgroup TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT	—	includeLeft_subgroup.eq_1 D_discrete
discrete_principalSubgroup 📖	—	—	—	—	NumberField.AdeleRing.discrete
existsE 📖	mathematical	—	NumberField.AdeleRing.instAlgebraRingOfIntegers_fLT TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT	—	TensorProduct.RightActions.instIsTopologicalAddGroup_fLT instBorelSpaceTensorProductRingOfIntegers_fLT TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT NumberField.AdeleRing.locallyCompactSpace not_injective_of_large_measure E_family_unbounded E_family_compact
incl_D𝔸quot_continuous 📖	mathematical	—	NumberField.AdeleRing.instAlgebraRingOfIntegers_fLT MeasureTheory.ringHaarChar_ker TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT TensorProduct.RightActions.instIsTopologicalRing_fLT_1 TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT NumberField.AdeleRing.locallyCompactSpace instMeasurableSpaceTensorProductRingOfIntegers_fLT instBorelSpaceTensorProductRingOfIntegers_fLT incl Dfx Df IsDedekindDomain.baseChangeAlgebra incl₁ incl_D𝔸quot	—	TensorProduct.RightActions.instIsTopologicalRing_fLT_1 TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT NumberField.AdeleRing.locallyCompactSpace instBorelSpaceTensorProductRingOfIntegers_fLT rest₁_continuous incl_D𝔸quot_equivariant
incl_D𝔸quot_equivariant 📖	mathematical	NumberField.AdeleRing.instAlgebraRingOfIntegers_fLT MeasureTheory.ringHaarChar_ker TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT TensorProduct.RightActions.instIsTopologicalRing_fLT_1 TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT NumberField.AdeleRing.locallyCompactSpace instMeasurableSpaceTensorProductRingOfIntegers_fLT instBorelSpaceTensorProductRingOfIntegers_fLT incl	Dfx Df IsDedekindDomain.baseChangeAlgebra incl₁ rest₁	—	TensorProduct.RightActions.instIsTopologicalRing_fLT_1 TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT NumberField.AdeleRing.locallyCompactSpace instBorelSpaceTensorProductRingOfIntegers_fLT
incl_D𝔸quot_surjective 📖	mathematical	—	NumberField.AdeleRing.instAlgebraRingOfIntegers_fLT MeasureTheory.ringHaarChar_ker TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT TensorProduct.RightActions.instIsTopologicalRing_fLT_1 TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT NumberField.AdeleRing.locallyCompactSpace instMeasurableSpaceTensorProductRingOfIntegers_fLT instBorelSpaceTensorProductRingOfIntegers_fLT incl Dfx Df IsDedekindDomain.baseChangeAlgebra incl₁ incl_D𝔸quot	—	TensorProduct.RightActions.instIsTopologicalRing_fLT_1 TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT NumberField.AdeleRing.locallyCompactSpace instBorelSpaceTensorProductRingOfIntegers_fLT incl_D𝔸quot_equivariant rest₁_surjective
incl₂_isClosedEmbedding 📖	mathematical	—	NumberField.AdeleRing.instAlgebraRingOfIntegers_fLT MeasureTheory.ringHaarChar_ker TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT TensorProduct.RightActions.instIsTopologicalRing_fLT_1 TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT NumberField.AdeleRing.locallyCompactSpace instMeasurableSpaceTensorProductRingOfIntegers_fLT instBorelSpaceTensorProductRingOfIntegers_fLT incl₂	—	TensorProduct.RightActions.instIsTopologicalRing_fLT_1 TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT NumberField.AdeleRing.locallyCompactSpace instBorelSpaceTensorProductRingOfIntegers_fLT instT2SpaceTensorProductRingOfIntegers_fLT
instBorelSpaceDf 📖	mathematical	—	Df TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT IsDedekindDomain.baseChangeAlgebra instMeasurableSpaceDf	—	—
instBorelSpaceDinf 📖	mathematical	—	Dinf TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT NumberField.InfiniteAdeleRing.instAlgebra_fLT_1 instMeasurableSpaceDinf	—	—
instBorelSpaceTensorProductRingOfIntegers_fLT 📖	mathematical	—	NumberField.AdeleRing.instAlgebraRingOfIntegers_fLT TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT instMeasurableSpaceTensorProductRingOfIntegers_fLT	—	—
instFiniteRealDinf 📖	mathematical	—	Dinf NumberField.InfiniteAdeleRing.instAlgebra_fLT_1 instAlgebraRealDinf	—	instIsScalarTowerRealInfiniteAdeleRingDinf instFiniteRealInfiniteAdeleRing_fLT TensorProduct.RightActions.instFinite_fLT
instIsModuleTopologyRealDinf 📖	mathematical	—	Dinf NumberField.InfiniteAdeleRing.instAlgebra_fLT_1 instAlgebraRealDinf TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT	—	IsModuleTopology.trans instIsScalarTowerRealInfiniteAdeleRingDinf instFiniteRealInfiniteAdeleRing_fLT instIsModuleTopologyRealInfiniteAdeleRing_fLT TensorProduct.RightActions.instIsModuleTopology_fLT
instIsModuleTopologyRingOfIntegersProdDinfDf 📖	mathematical	—	Dinf Df NumberField.InfiniteAdeleRing.instAlgebra_fLT_1 IsDedekindDomain.baseChangeAlgebra instModuleRingOfIntegersProdDinfDf TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT	—	IsModuleTopology.instProd' TensorProduct.RightActions.instIsModuleTopology_fLT
instIsScalarTowerRealInfiniteAdeleRingDinf 📖	mathematical	—	Dinf instAlgebraRealInfiniteAdeleRing_fLT TensorProduct.RightActions.instSMul_fLT NumberField.InfiniteAdeleRing.instAlgebra_fLT_1 instAlgebraRealDinf	—	—
instSecondCountableTopologyDinf 📖	mathematical	—	Dinf TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT NumberField.InfiniteAdeleRing.instAlgebra_fLT_1	—	Module.Finite.secondCountabletopology instFiniteRealDinf instIsModuleTopologyRealDinf
instT2SpaceTensorProductRingOfIntegers_fLT 📖	mathematical	—	NumberField.AdeleRing.instAlgebraRingOfIntegers_fLT TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT	—	IsModuleTopology.t2Space TensorProduct.RightActions.instFree_fLT instT2SpaceAdeleRingRingOfIntegers_fLT TensorProduct.RightActions.instIsModuleTopology_fLT
not_injective_of_large_measure 📖	mathematical	—	NumberField.AdeleRing.instAlgebraRingOfIntegers_fLT	—	discrete_includeLeft_subgroup instSecondCountableTopologyAdeleRingRingOfIntegers_fLT polish_of_locally_compact_second_countable instT2SpaceTensorProductRingOfIntegers_fLT TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT NumberField.AdeleRing.locallyCompactSpace TopologicalAddGroup.IsSES.not_injOn_of_measure_gt TensorProduct.RightActions.instIsTopologicalAddGroup_fLT instBorelSpaceTensorProductRingOfIntegers_fLT compact_includeLeft_subgroup
rest₁_continuous 📖	mathematical	—	NumberField.AdeleRing.instAlgebraRingOfIntegers_fLT MeasureTheory.ringHaarChar_ker TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT TensorProduct.RightActions.instIsTopologicalRing_fLT_1 TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT NumberField.AdeleRing.locallyCompactSpace instMeasurableSpaceTensorProductRingOfIntegers_fLT instBorelSpaceTensorProductRingOfIntegers_fLT Dfx Df IsDedekindDomain.baseChangeAlgebra rest₁	—	TensorProduct.RightActions.instIsTopologicalRing_fLT_1 TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT NumberField.AdeleRing.locallyCompactSpace instBorelSpaceTensorProductRingOfIntegers_fLT D𝔸_prodRight_units_cont
rest₁_surjective 📖	mathematical	—	NumberField.AdeleRing.instAlgebraRingOfIntegers_fLT MeasureTheory.ringHaarChar_ker TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT TensorProduct.RightActions.instIsTopologicalRing_fLT_1 TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT NumberField.AdeleRing.locallyCompactSpace instMeasurableSpaceTensorProductRingOfIntegers_fLT instBorelSpaceTensorProductRingOfIntegers_fLT Dfx rest₁	—	TensorProduct.RightActions.instIsTopologicalRing_fLT_1 TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT NumberField.AdeleRing.locallyCompactSpace instBorelSpaceTensorProductRingOfIntegers_fLT ringHaarChar_D𝔸_prodRight_units_aux rest₁.eq_1
ringHaarChar_D𝔸 📖	mathematical	—	NumberField.AdeleRing.instAlgebraRingOfIntegers_fLT TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT MeasureTheory.ringHaarChar TensorProduct.RightActions.instIsTopologicalRing_fLT_1 TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT NumberField.AdeleRing.locallyCompactSpace instMeasurableSpaceTensorProductRingOfIntegers_fLT instBorelSpaceTensorProductRingOfIntegers_fLT Dinfx Dfx Dinf NumberField.InfiniteAdeleRing.instAlgebra_fLT_1 Df IsDedekindDomain.baseChangeAlgebra D𝔸_prodRight_units instLocallyCompactSpaceFiniteAdeleRingRingOfIntegers_fLT instMeasurableSpaceDinf instMeasurableSpaceDf instBorelSpaceDinf instBorelSpaceDf instSecondCountableTopologyDinf	—	MeasureTheory.addEquivAddHaarChar_eq_addEquivAddHaarChar_of_continuousAddEquiv TensorProduct.RightActions.instIsTopologicalAddGroup_fLT TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT NumberField.AdeleRing.locallyCompactSpace instBorelSpaceTensorProductRingOfIntegers_fLT instLocallyCompactSpaceFiniteAdeleRingRingOfIntegers_fLT instBorelSpaceDinf instBorelSpaceDf instSecondCountableTopologyDinf TensorProduct.RightActions.instIsTopologicalRing_fLT_1
ringHaarChar_D𝔸_prodRight_units_aux 📖	mathematical	—	NumberField.AdeleRing.instAlgebraRingOfIntegers_fLT TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT MeasureTheory.ringHaarChar TensorProduct.RightActions.instIsTopologicalRing_fLT_1 TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT NumberField.AdeleRing.locallyCompactSpace instMeasurableSpaceTensorProductRingOfIntegers_fLT instBorelSpaceTensorProductRingOfIntegers_fLT Dinfx Dfx Dinf NumberField.InfiniteAdeleRing.instAlgebra_fLT_1 Df IsDedekindDomain.baseChangeAlgebra D𝔸_prodRight_units	—	TensorProduct.RightActions.instIsTopologicalRing_fLT_1 TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT NumberField.AdeleRing.locallyCompactSpace instBorelSpaceTensorProductRingOfIntegers_fLT ringHaarChar_D𝔸_real_surjective
ringHaarChar_D𝔸_real_surjective 📖	mathematical	—	NumberField.AdeleRing.instAlgebraRingOfIntegers_fLT TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT MeasureTheory.ringHaarChar TensorProduct.RightActions.instIsTopologicalRing_fLT_1 TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT NumberField.AdeleRing.locallyCompactSpace instMeasurableSpaceTensorProductRingOfIntegers_fLT instBorelSpaceTensorProductRingOfIntegers_fLT Dinfx Dfx Dinf NumberField.InfiniteAdeleRing.instAlgebra_fLT_1 Df IsDedekindDomain.baseChangeAlgebra D𝔸_prodRight_units instAlgebraRealDinf	—	instFiniteRealDinf instNontrivialTensorProductOfFree_fLT_1 TensorProduct.RightActions.instIsTopologicalRing_fLT_1 TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT instBorelSpaceDinf MeasureTheory.ringHaarChar_ModuleFinite_unit instIsModuleTopologyRealDinf NumberField.AdeleRing.locallyCompactSpace instBorelSpaceTensorProductRingOfIntegers_fLT instLocallyCompactSpaceFiniteAdeleRingRingOfIntegers_fLT instBorelSpaceDf instSecondCountableTopologyDinf ringHaarChar_D𝔸 MeasureTheory.ringHaarChar_prod MeasureTheory.ringHaarChar_real
smul_D𝔸_prodRight_symm 📖	mathematical	—	NumberField.AdeleRing.instAlgebraRingOfIntegers_fLT Dinfx Dfx Dinf NumberField.InfiniteAdeleRing.instAlgebra_fLT_1 Df IsDedekindDomain.baseChangeAlgebra D𝔸_prodRight_units D𝔸_prodRight	—	—
toQuot_cont 📖	mathematical	—	NumberField.AdeleRing.instAlgebraRingOfIntegers_fLT MeasureTheory.ringHaarChar_ker TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT TensorProduct.RightActions.instIsTopologicalRing_fLT_1 TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT NumberField.AdeleRing.locallyCompactSpace instMeasurableSpaceTensorProductRingOfIntegers_fLT instBorelSpaceTensorProductRingOfIntegers_fLT incl toQuot	—	TensorProduct.RightActions.instIsTopologicalRing_fLT_1 TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT NumberField.AdeleRing.locallyCompactSpace instBorelSpaceTensorProductRingOfIntegers_fLT
toQuot_surjective 📖	mathematical	—	NumberField.AdeleRing.instAlgebraRingOfIntegers_fLT MeasureTheory.ringHaarChar_ker TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT TensorProduct.RightActions.instIsTopologicalRing_fLT_1 TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT NumberField.AdeleRing.locallyCompactSpace instMeasurableSpaceTensorProductRingOfIntegers_fLT instBorelSpaceTensorProductRingOfIntegers_fLT incl toQuot M	—	TensorProduct.RightActions.instIsTopologicalRing_fLT_1 TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT NumberField.AdeleRing.locallyCompactSpace instBorelSpaceTensorProductRingOfIntegers_fLT antidiag_mem_C

NumberField.AdeleRing.DivisionAlgebra.Aux.Uf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
spec 📖	mathematical	—	IsDedekindDomain.baseChangeAlgebra TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT NumberField.AdeleRing.DivisionAlgebra.Aux.Uf	—	TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT instLocallyCompactSpaceFiniteAdeleRingRingOfIntegers_fLT

NumberField.AdeleRing.DivisionAlgebra.Aux.Ui

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
spec 📖	mathematical	—	NumberField.InfiniteAdeleRing.instAlgebra_fLT_1 TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT NumberField.AdeleRing.DivisionAlgebra.Aux.Ui	—	TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT

NumberField.FiniteAdeleRing.DivisionAlgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finiteDoubleCoset 📖	mathematical	NumberField.AdeleRing.DivisionAlgebra.Aux.Dfx NumberField.AdeleRing.DivisionAlgebra.Aux.Df TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT IsDedekindDomain.baseChangeAlgebra	NumberField.AdeleRing.DivisionAlgebra.Aux.incl₁	—	units_cocompact TensorProduct.RightActions.instIsTopologicalRing_fLT_1 DoubleCoset.union_image_mk_rightRel DoubleCoset.iUnion_finset_quotTodoubleCoset DoubleCoset.union_finset_rightrel_cover
units_cocompact 📖	mathematical	—	NumberField.AdeleRing.DivisionAlgebra.Aux.Dfx NumberField.AdeleRing.DivisionAlgebra.Aux.Df IsDedekindDomain.baseChangeAlgebra NumberField.AdeleRing.DivisionAlgebra.Aux.incl₁ TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT	—	TensorProduct.RightActions.instIsTopologicalRing_fLT_1 TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT NumberField.AdeleRing.locallyCompactSpace NumberField.AdeleRing.DivisionAlgebra.Aux.instBorelSpaceTensorProductRingOfIntegers_fLT NumberField.AdeleRing.DivisionAlgebra.compact_quotient NumberField.AdeleRing.DivisionAlgebra.Aux.incl_D𝔸quot_continuous NumberField.AdeleRing.DivisionAlgebra.Aux.incl_D𝔸quot_surjective

NumberField.InfiniteAdeleRing

Definitions

Name	Category	Theorems
Dinf_tensorPi_equiv_piTensor 📖	CompOp	—
Dinf_tensorPi_equiv_piTensor_aux 📖	CompOp	—
Dinf_tensorPi_equiv_piTensor_mulEquiv 📖	CompOp	—
instAlgebraRealCompletion_fLT 📖	CompOp	6 math math: instIsModuleTopologyRealCompletion_fLT, instFiniteRealCompletion_fLT, algebraMap_completion_def, algebraMap_completion, instContinuousSMulRealCompletion_fLT, instIsScalarTowerRealCompletionTensorProduct_fLT
instAlgebraRealTensorProductCompletion_fLT 📖	CompOp	3 math math: instIsModuleTopologyRealTensorProductCompletion_fLT, instIsModuleTopologyRealForallTensorProductCompletion_fLT, instIsScalarTowerRealCompletionTensorProduct_fLT
real_to_completion 📖	CompOp	1 math math: algebraMap_completion_def

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_completion 📖	mathematical	—	instAlgebraRealInfiniteAdeleRing_fLT instAlgebraRealCompletion_fLT	—	—
algebraMap_completion_def 📖	mathematical	—	instAlgebraRealCompletion_fLT real_to_completion	—	—
instContinuousSMulRealCompletion_fLT 📖	mathematical	—	instAlgebraRealCompletion_fLT	—	algebraMap_completion_def
instFiniteRealCompletion_fLT 📖	mathematical	—	instAlgebraRealCompletion_fLT	—	—
instIsModuleTopologyRealCompletion_fLT 📖	mathematical	—	instAlgebraRealCompletion_fLT	—	instContinuousSMulRealCompletion_fLT instFiniteRealCompletion_fLT
instIsModuleTopologyRealForallTensorProductCompletion_fLT 📖	mathematical	—	WithAbs.instUniformContinuousConstSMulReal_fLT instAlgebraRealTensorProductCompletion_fLT TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT	—	WithAbs.instUniformContinuousConstSMulReal_fLT instIsModuleTopologyRealTensorProductCompletion_fLT
instIsModuleTopologyRealTensorProductCompletion_fLT 📖	mathematical	—	WithAbs.instUniformContinuousConstSMulReal_fLT instAlgebraRealTensorProductCompletion_fLT TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT	—	WithAbs.instUniformContinuousConstSMulReal_fLT IsModuleTopology.trans instIsScalarTowerRealCompletionTensorProduct_fLT instFiniteRealCompletion_fLT instIsModuleTopologyRealCompletion_fLT TensorProduct.RightActions.instIsModuleTopology_fLT
instIsScalarTowerRealCompletionTensorProduct_fLT 📖	mathematical	—	WithAbs.instUniformContinuousConstSMulReal_fLT instAlgebraRealCompletion_fLT TensorProduct.RightActions.instSMul_fLT instAlgebraRealTensorProductCompletion_fLT	—	WithAbs.instUniformContinuousConstSMulReal_fLT
instSecondCountableTopologyTensorProductCompletion_fLT 📖	mathematical	—	WithAbs.instUniformContinuousConstSMulReal_fLT TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT	—	Module.Finite.secondCountabletopology WithAbs.instUniformContinuousConstSMulReal_fLT instSecondCountableTopologyCompletion_fLT TensorProduct.RightActions.instFinite_fLT TensorProduct.RightActions.instIsModuleTopology_fLT
isCentralSimple_infinite_addHaarScalarFactor_left_mul_eq_right_mul 📖	mathematical	—	NumberField.AdeleRing.DivisionAlgebra.Aux.Dinf instAlgebra_fLT_1 TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT NumberField.AdeleRing.DivisionAlgebra.Aux.instMeasurableSpaceDinf NumberField.AdeleRing.DivisionAlgebra.Aux.instBorelSpaceDinf TensorProduct.RightActions.instIsTopologicalAddGroup_fLT TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT ContinuousAddEquiv.mulLeft TensorProduct.RightActions.instIsTopologicalRing_fLT_1 ContinuousAddEquiv.mulRight	—	WithAbs.instUniformContinuousConstSMulReal_fLT NumberField.AdeleRing.DivisionAlgebra.Aux.instBorelSpaceDinf TensorProduct.RightActions.instIsTopologicalAddGroup_fLT TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT TensorProduct.RightActions.instIsTopologicalRing_fLT_1 instSecondCountableTopologyTensorProductCompletion_fLT MeasureTheory.addEquivAddHaarChar_eq_addEquivAddHaarChar_of_continuousAddEquiv tensorPi_equiv_piTensor_map_mul isCentralSimple_infinite_addHaarScalarFactor_left_mul_eq_right_mul_aux
isCentralSimple_infinite_addHaarScalarFactor_left_mul_eq_right_mul_aux 📖	mathematical	WithAbs.instUniformContinuousConstSMulReal_fLT TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT	instSecondCountableTopologyTensorProductCompletion_fLT TensorProduct.RightActions.instIsTopologicalAddGroup_fLT TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT ContinuousAddEquiv.mulLeft TensorProduct.RightActions.instIsTopologicalRing_fLT_1 ContinuousAddEquiv.mulRight	—	WithAbs.instUniformContinuousConstSMulReal_fLT instSecondCountableTopologyTensorProductCompletion_fLT TensorProduct.RightActions.instIsTopologicalAddGroup_fLT TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT TensorProduct.RightActions.instIsTopologicalRing_fLT_1 MeasureTheory.addEquivAddHaarChar_piCongrRight IsSimpleRing.ringHaarChar_eq_addEquivAddHaarChar_mulRight instBorelSpaceCompletion_fLT TensorProduct.RightActions.instFinite_fLT instIsSimpleRingTensorProductOfIsCentral_fLT TensorProduct.RightActions.instIsModuleTopology_fLT instIsCentralTensorProduct_fLT_1 instSecondCountableTopologyCompletion_fLT
tensorPi_equiv_piTensor_map_mul 📖	mathematical	—	WithAbs.instUniformContinuousConstSMulReal_fLT tensorPi_equiv_piTensor NumberField.AdeleRing.DivisionAlgebra.Aux.Dinf instAlgebra_fLT_1	—	WithAbs.instUniformContinuousConstSMulReal_fLT tensorPi_equiv_piTensor_apply

(root)

Definitions

Name	Category	Theorems
termD_𝔸 📖	CompOp	—

---

← Back to Index