Documentation Verification Report

RightActionInstances

πŸ“ Source: FLT/Hacks/RightActionInstances.lean

Statistics

MetricCount
Definitionsbasis, comm, baseChange, baseChange, baseChange, comm, instAlgebra_fLT, instModule_fLT, instSMul_fLT, instTopologicalSpaceOfFinite_fLT
10
Theoremscomm_apply_tmul, comm_symm_apply_tmul, baseChange_comp, baseChange_id, comm_apply_tmul, comm_symm_apply_tmul, algebraMap_eval, instFinite_fLT, instFree_fLT, instIsModuleTopology_fLT, instIsScalarTower_fLT, instIsTopologicalAddGroup_fLT, instIsTopologicalRing_fLT, instIsTopologicalRing_fLT_1, instLocallyCompactSpaceOfIsTopologicalRing_fLT, smul_def
16
Total26

TensorProduct.RightActions

Definitions

NameCategoryTheorems
instAlgebra_fLT πŸ“–CompOp
10 mathmath: IsDedekindDomain.HeightOneSpectrum.finrank_tensorProduct_adicCompletion_eq_finrank_pi_adicCompletion, IsDedekindDomain.HeightOneSpectrum.Rigidification.continuous_toFun, algebraMap_eval, SemialgHom.baseChangeRightOfAlgebraMap_coe, SemialgHom.baseChangeRightOfAlgebraMap_apply, instIsCentralTensorProduct_fLT_1, Algebra.TensorProduct.comm_symm_apply_tmul, Algebra.TensorProduct.comm_apply_tmul, IsDedekindDomain.HeightOneSpectrum.Rigidification.continuous_invFun, NumberField.AdeleRing.baseChangeAdeleAlgHom_bijective
instModule_fLT πŸ“–CompOp
20 mathmath: instFinite_fLT, MeasureTheory.addHaarScalarFactor_tensor_adeles_eq_one, NumberField.AdeleRing.ModuleBaseChangeContinuousSemilinearMap_apply, IsDedekindDomain.HeightOneSpectrum.tensorAdicCompletionComapLinearMap_isOpenQuotientMap, IsDedekindDomain.HeightOneSpectrum.adicCompletionComapIntegerLinearMap_range_eq_integers, NumberField.InfiniteAdeleRing.instFreeTensorProduct_fLT, Module.TensorProduct.comm_apply_tmul, ContinuousLinearEquiv.baseChange_apply, instFree_fLT, Module.Basis.rightBaseChange_apply, LinearMap.baseChange_comp, LinearMap.baseChange_id, MeasureTheory.addHaarScalarFactor_tensor_adeles_rat_eq_one, NumberField.AdeleRing.moduleBaseChangeContinuousAddEquiv_apply_eq_moduleBaseChangeAddEquiv'_apply, Module.TensorProduct.comm_symm_apply_tmul, Module.Basis.rightBaseChange_repr, TensorProduct.finrank_rightAlgebra, NumberField.AdeleRing.DivisionAlgebra.Aux.D_discrete_aux, IsDedekindDomain.HeightOneSpectrum.tensorAdicCompletionComapLinearMap_surjective, NumberField.InfinitePlace.Completion.finrank_pi_eq_finrank_tensorProduct
instSMul_fLT πŸ“–CompOp
6 mathmath: NumberField.AdeleRing.DivisionAlgebra.Aux.instIsScalarTowerRealInfiniteAdeleRingDinf, smul_def, instIsScalarTower_fLT, instIsModuleTopology_fLT, NumberField.InfinitePlace.Completion.instIsModuleTopologyTensorProduct_fLT, NumberField.InfiniteAdeleRing.instIsScalarTowerRealCompletionTensorProduct_fLT
instTopologicalSpaceOfFinite_fLT πŸ“–CompOp
65 mathmath: NumberField.AdeleRing.DivisionAlgebra.Aux.T_finite_extracted1, MeasureTheory.addHaarScalarFactor_tensor_adeles_eq_one, NumberField.AdeleRing.DivisionAlgebra.Aux.compact_includeLeft_subgroup, NumberField.AdeleRing.DivisionAlgebra.Aux.C_compact, IsDedekindDomain.HeightOneSpectrum.Rigidification.continuous_toFun, NumberField.AdeleRing.DivisionAlgebra.Aux.X_compact, IsDedekindDomain.HeightOneSpectrum.tensorAdicCompletionComapLinearMap_isOpenQuotientMap, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.U1_compact, instIsTopologicalRing_fLT, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.right_invt, NumberField.AdeleRing.DivisionAlgebra.Aux.incl_D𝔸quot_surjective, instLocallyCompactSpaceOfIsTopologicalRing_fLT, NumberField.AdeleRing.DivisionAlgebra.Aux.instIsModuleTopologyRealDinf, NumberField.InfiniteAdeleRing.instIsModuleTopologyRealTensorProductCompletion_fLT, NumberField.AdeleRing.DivisionAlgebra.Aux.Y_compact, IsDedekindDomain.HeightOneSpectrum.tensorAdicCompletionIsClopenRange, ContinuousLinearEquiv.baseChange_apply, NumberField.AdeleRing.DivisionAlgebra.Aux.ringHaarChar_D𝔸, NumberField.AdeleRing.DivisionAlgebra.Aux.Ui.spec, NumberField.AdeleRing.DivisionAlgebra.Aux.incl_D𝔸quot_continuous, NumberField.AdeleRing.DivisionAlgebra.Aux.discrete_includeLeft_subgroup, NumberField.AdeleRing.DivisionAlgebra.Aux.E_family_compact, NumberField.InfiniteAdeleRing.isCentralSimple_infinite_addHaarScalarFactor_left_mul_eq_right_mul, IsDedekindDomain.HeightOneSpectrum.tensorAdicCompletionIntegersToRange_eq_closureIntegers, NumberField.AdeleRing.DivisionAlgebra.Aux.instBorelSpaceDf, NumberField.AdeleRing.DivisionAlgebra.Aux.E_compact, IsDedekindDomain.HeightOneSpectrum.tensorAdicCompletionIntegersToRange_subset_closureIntegers, NumberField.AdeleRing.DivisionAlgebra.Aux.toQuot_cont, NumberField.AdeleRing.DivisionAlgebra.Aux.instIsModuleTopologyRingOfIntegersProdDinfDf, NumberField.AdeleRing.baseChangeEquiv_tsum_apply_right, NumberField.AdeleRing.DivisionAlgebra.Aux.instBorelSpaceTensorProductRingOfIntegers_fLT, instIsModuleTopology_fLT, NumberField.AdeleRing.units_mem_ringHaarCharacter_ker, NumberField.InfiniteAdeleRing.instSecondCountableTopologyTensorProductCompletion_fLT, NumberField.AdeleRing.DivisionAlgebra.Aux.ImAux_isCompact, NumberField.AdeleRing.DivisionAlgebra.Aux.toQuot_surjective, NumberField.AdeleRing.isCentralSimple_addHaarScalarFactor_left_mul_eq_right_mul, NumberField.AdeleRing.addEquivAddHaarChar_mulRight_unit_eq_one, MeasureTheory.addHaarScalarFactor_tensor_adeles_rat_eq_one, NumberField.AdeleRing.DivisionAlgebra.Aux.D𝔸_prodRight_units_cont, NumberField.AdeleRing.DivisionAlgebra.Aux.ringHaarChar_D𝔸_prodRight_units_aux, NumberField.AdeleRing.DivisionAlgebra.Aux.instT2SpaceTensorProductRingOfIntegers_fLT, NumberField.AdeleRing.DivisionAlgebra.compact_quotient, NumberField.AdeleRing.moduleBaseChangeContinuousAddEquiv_apply_eq_moduleBaseChangeAddEquiv'_apply, NumberField.AdeleRing.DivisionAlgebra.Aux.rest₁_surjective, instIsTopologicalAddGroup_fLT, NumberField.AdeleRing.DivisionAlgebra.Aux.rest₁_continuous, NumberField.AdeleRing.DivisionAlgebra.Aux.ringHaarChar_D𝔸_real_surjective, NumberField.AdeleRing.DivisionAlgebra.Aux.instSecondCountableTopologyDinf, NumberField.FiniteAdeleRing.isCentralSimple_addHaarScalarFactor_left_mul_eq_right_mul, IsDedekindDomain.HeightOneSpectrum.Rigidification.continuous_invFun, NumberField.AdeleRing.DivisionAlgebra.Aux.M_compact, NumberField.AdeleRing.DivisionAlgebra.Aux.inclβ‚‚_isClosedEmbedding, NumberField.AdeleRing.DivisionAlgebra.Aux.E_family_unbounded, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.U1_open, IsDedekindDomain.HeightOneSpectrum.adicCompletionComapAlgHom_map_closure_is_closed, NumberField.AdeleRing.DivisionAlgebra.Aux.E_family_nonempty_interior, NumberField.AdeleRing.DivisionAlgebra.Aux.D_discrete, NumberField.AdeleRing.DivisionAlgebra.Aux.D_discrete_aux, NumberField.FiniteAdeleRing.DivisionAlgebra.units_cocompact, NumberField.InfiniteAdeleRing.instIsModuleTopologyRealForallTensorProductCompletion_fLT, NumberField.AdeleRing.DivisionAlgebra.Aux.Uf.spec, NumberField.AdeleRing.DivisionAlgebra.Aux.existsE, NumberField.AdeleRing.DivisionAlgebra.Aux.instBorelSpaceDinf, instIsTopologicalRing_fLT_1

Theorems

NameKindAssumesProvesValidatesDepends On
algebraMap_eval πŸ“–mathematicalβ€”instAlgebra_fLTβ€”β€”
instFinite_fLT πŸ“–mathematicalβ€”instModule_fLTβ€”β€”
instFree_fLT πŸ“–mathematicalβ€”instModule_fLTβ€”β€”
instIsModuleTopology_fLT πŸ“–mathematicalβ€”instSMul_fLT
instTopologicalSpaceOfFinite_fLT		β€”β€”
instIsScalarTower_fLT πŸ“–mathematicalβ€”instSMul_fLTβ€”β€”
instIsTopologicalAddGroup_fLT πŸ“–mathematicalβ€”instTopologicalSpaceOfFinite_fLTβ€”instIsModuleTopology_fLT
instIsTopologicalRing_fLT πŸ“–mathematicalβ€”instTopologicalSpaceOfFinite_fLTβ€”IsModuleTopology.Module.topologicalRing
instFinite_fLT
instIsModuleTopology_fLT
instIsTopologicalRing_fLT_1 πŸ“–mathematicalβ€”instTopologicalSpaceOfFinite_fLTβ€”IsModuleTopology.Module.topologicalRing
instFinite_fLT
instIsModuleTopology_fLT
instLocallyCompactSpaceOfIsTopologicalRing_fLT πŸ“–mathematicalβ€”instTopologicalSpaceOfFinite_fLTβ€”IsModuleTopology.locallyCompactSpaceOfFinite
instIsModuleTopology_fLT
instFinite_fLT
smul_def πŸ“–mathematicalβ€”instSMul_fLTβ€”β€”

TensorProduct.RightActions.Algebra.TensorProduct

Definitions

NameCategoryTheorems
basis πŸ“–CompOpβ€”
comm πŸ“–CompOp
2 mathmath: comm_symm_apply_tmul, comm_apply_tmul

Theorems

NameKindAssumesProvesValidatesDepends On
comm_apply_tmul πŸ“–mathematicalβ€”TensorProduct.RightActions.instAlgebra_fLT
comm		β€”β€”
comm_symm_apply_tmul πŸ“–mathematicalβ€”TensorProduct.RightActions.instAlgebra_fLT
comm		β€”β€”

TensorProduct.RightActions.AlgebraMap

Definitions

NameCategoryTheorems
baseChange πŸ“–CompOpβ€”

TensorProduct.RightActions.LinearEquiv

Definitions

NameCategoryTheorems
baseChange πŸ“–CompOpβ€”

TensorProduct.RightActions.LinearMap

Definitions

NameCategoryTheorems
baseChange πŸ“–CompOp
2 mathmath: baseChange_comp, baseChange_id

Theorems

NameKindAssumesProvesValidatesDepends On
baseChange_comp πŸ“–mathematicalβ€”TensorProduct.RightActions.instModule_fLT
baseChange		β€”β€”
baseChange_id πŸ“–mathematicalβ€”baseChange
TensorProduct.RightActions.instModule_fLT		β€”β€”

TensorProduct.RightActions.Module.TensorProduct

Definitions

NameCategoryTheorems
comm πŸ“–CompOp
2 mathmath: comm_apply_tmul, comm_symm_apply_tmul

Theorems

NameKindAssumesProvesValidatesDepends On
comm_apply_tmul πŸ“–mathematicalβ€”TensorProduct.RightActions.instModule_fLT
comm		β€”β€”
comm_symm_apply_tmul πŸ“–mathematicalβ€”TensorProduct.RightActions.instModule_fLT
comm		β€”β€”

---

← Back to Index