InfiniteAdeleRing

📁 Source: FLT/NumberField/InfiniteAdeleRing.lean

Statistics

Metric	Count
Definitions baseChange, baseChangeEquiv, baseChangeEquivAux, instAlgebraForallCompletion_fLT, instAlgebra_fLT, instAlgebra_fLT_1, piEquiv	7
Theorems baseChangeEquivAux_apply, baseChangeEquivAux_coe_eq_baseChange_of_algebraMap, baseChangeEquivAux_tmul, baseChange_cont, instFiberwiseSMulInfinitePlaceCompletion, instFreeTensorProduct_fLT, instIsModuleTopology_fLT, instIsScalarTower_fLT, instIsScalarTower_fLT_1	9
Total	16

NumberField.InfiniteAdeleRing

Definitions

Name	Category	Theorems
baseChange 📖	CompOp	4 math math: baseChangeEquivAux_apply, baseChange_cont, baseChangeEquivAux_tmul, baseChangeEquivAux_coe_eq_baseChange_of_algebraMap
baseChangeEquiv 📖	CompOp	—
baseChangeEquivAux 📖	CompOp	3 math math: baseChangeEquivAux_apply, baseChangeEquivAux_tmul, baseChangeEquivAux_coe_eq_baseChange_of_algebraMap
instAlgebraForallCompletion_fLT 📖	CompOp	1 math math: instFiberwiseSMulInfinitePlaceCompletion
instAlgebra_fLT 📖	CompOp	2 math math: instIsModuleTopology_fLT, instIsScalarTower_fLT_1
instAlgebra_fLT_1 📖	CompOp	21 math math: NumberField.AdeleRing.DivisionAlgebra.Aux.instIsScalarTowerRealInfiniteAdeleRingDinf, tensorPi_equiv_piTensor_map_mul, Rat.InfiniteAdeleRing.exists_sub_norm_le_one, instFreeTensorProduct_fLT, NumberField.AdeleRing.DivisionAlgebra.Aux.instIsModuleTopologyRealDinf, NumberField.AdeleRing.DivisionAlgebra.Aux.ringHaarChar_D𝔸, NumberField.AdeleRing.DivisionAlgebra.Aux.Ui.spec, instIsScalarTower_fLT, isCentralSimple_infinite_addHaarScalarFactor_left_mul_eq_right_mul, NumberField.AdeleRing.DivisionAlgebra.Aux.smul_D𝔸_prodRight_symm, NumberField.AdeleRing.DivisionAlgebra.Aux.instIsModuleTopologyRingOfIntegersProdDinfDf, baseChangeEquivAux_apply, baseChangeEquivAux_tmul, instIsScalarTower_fLT_1, NumberField.AdeleRing.DivisionAlgebra.Aux.instFiniteRealDinf, NumberField.AdeleRing.DivisionAlgebra.Aux.D𝔸_prodRight_units_cont, NumberField.AdeleRing.DivisionAlgebra.Aux.ringHaarChar_D𝔸_prodRight_units_aux, NumberField.AdeleRing.DivisionAlgebra.Aux.ringHaarChar_D𝔸_real_surjective, NumberField.AdeleRing.DivisionAlgebra.Aux.instSecondCountableTopologyDinf, baseChangeEquivAux_coe_eq_baseChange_of_algebraMap, NumberField.AdeleRing.DivisionAlgebra.Aux.instBorelSpaceDinf
piEquiv 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
baseChangeEquivAux_apply 📖	mathematical	—	instAlgebra_fLT_1 baseChangeEquivAux SemialgHom.baseChange_of_algebraMap baseChange	—	baseChangeEquivAux_coe_eq_baseChange_of_algebraMap
baseChangeEquivAux_coe_eq_baseChange_of_algebraMap 📖	mathematical	—	instAlgebra_fLT_1 baseChangeEquivAux SemialgHom.baseChange_of_algebraMap baseChange	—	instIsScalarTower_fLT baseChangeEquivAux_tmul SemialgHom.baseChange_of_algebraMap_tmul
baseChangeEquivAux_tmul 📖	mathematical	—	instAlgebra_fLT_1 baseChangeEquivAux SemialgHom instFunLike baseChange	—	—
baseChange_cont 📖	mathematical	—	SemialgHom instFunLike baseChange	—	Continuous.piSemialgHomPi NumberField.InfinitePlace.Completion.comapHom_cont
instFiberwiseSMulInfinitePlaceCompletion 📖	mathematical	—	Pi.FiberwiseSMul NumberField.InfinitePlace.Completion.instNormedSpaceValEqComapAlgebraMap_fLT instAlgebraForallCompletion_fLT	—	—
instFreeTensorProduct_fLT 📖	mathematical	—	instAlgebra_fLT_1 TensorProduct.RightActions.instModule_fLT	—	—
instIsModuleTopology_fLT 📖	mathematical	—	instAlgebra_fLT	—	—
instIsScalarTower_fLT 📖	mathematical	—	instAlgebra_fLT_1	—	WithAbs.instUniformContinuousConstSMulReal_fLT WithAbs.instIsScalarTowerReal_fLT
instIsScalarTower_fLT_1 📖	mathematical	—	instAlgebra_fLT_1 instAlgebra_fLT	—	instIsScalarTower_fLT SemialgHomClass.toRingHomClass SemialgHomClass.instSemialgHom SemialgHom.toRingHom_eq_coe SemialgHom.commutes

---

← Back to Index