Documentation Verification Report

WithVal

📁 Source: FLT/Mathlib/Topology/Algebra/Valued/WithVal.lean

Statistics

Metric	Count
Definitions `instAlgebraWithVal_fLT`, `instAlgebraWithVal_fLT_1`	2
Theorems `instIsScalarTowerWithVal_fLT`, `instIsScalarTowerWithVal_fLT_1`	2
Total	4

(root)

Definitions

Name	Category	Theorems
`instAlgebraWithVal_fLT` 📖	CompOp	7 math math: `IsDedekindDomain.cofinite_mapsTo_adicCompletionComapSemialgHom`, `IsDedekindDomain.HeightOneSpectrum.adicCompletionComapSemialgHom.mapadicCompletionIntegers`, `IsDedekindDomain.HeightOneSpectrum.valued_adicCompletionComap`, `IsDedekindDomain.HeightOneSpectrum.comap_integer_algebraMap`, `instIsScalarTowerWithVal_fLT`, `IsDedekindDomain.HeightOneSpectrum.adicCompletionComapSemialgHom_continuous`, `IsDedekindDomain.HeightOneSpectrum.adicCompletionComap_coe`
`instAlgebraWithVal_fLT_1` 📖	CompOp	25 math math: `IsDedekindDomain.HeightOneSpectrum.adicCompletionComapIntegerLinearEquiv_bijOn`, `IsDedekindDomain.HeightOneSpectrum.tensorAdicCompletionComapAlgHom_bijective`, `IsDedekindDomain.HeightOneSpectrum.tensorAdicCompletionComapLinearMap_isOpenQuotientMap`, `instBorelSpaceTensorProductAdicCompletionRingOfIntegers_fLT`, `IsDedekindDomain.HeightOneSpectrum.tensorAdicCompletionIsClopenRange`, `IsDedekindDomain.HeightOneSpectrum.adicCompletionComapAlgEquiv_integral`, `IsDedekindDomain.HeightOneSpectrum.tensorAdicCompletionIntegersTo_tmul`, `IsDedekindDomain.HeightOneSpectrum.tensorAdicCompletionIntegersToRange_eq_closureIntegers`, `IsDedekindDomain.HeightOneSpectrum.tensorAdicCompletionIntegersToRange_subset_closureIntegers`, `instIsTopologicalAddGroupTensorProductAdicCompletionRingOfIntegers_fLT`, `instIsModuleTopologyAdicCompletionRingOfIntegersTensorProduct_fLT`, `IsDedekindDomain.range_adicCompletionTensorIntegerCoe_eq_lTensorRestriction`, `IsDedekindDomain.HeightOneSpectrum.adicCompletionComapIntegerLinearEquiv_tmul_apply`, `IsDedekindDomain.FiniteAdeleRing.restrictedProduct_prod_equiv_apply`, `IsDedekindDomain.FiniteAdeleRing.tensorEquivRestrictedProduct_tmul`, `IsDedekindDomain.HeightOneSpectrum.instMulActionHomClassAlgHomTensorProductAdicCompletionForallValEqComap`, `instIsTopologicalRingTensorProductAdicCompletionRingOfIntegers_fLT`, `instLocallyCompactSpaceTensorProductAdicCompletionRingOfIntegers_fLT`, `IsDedekindDomain.FiniteAdeleRing.restrictedProduct_tensorProduct_equiv_restrictedProduct_prod_apply`, `FiniteAdeleRing.Aux.e_commSq`, `IsDedekindDomain.HeightOneSpectrum.instOneHomClassAlgHomTensorProductAdicCompletionForallValEqComap`, `IsDedekindDomain.HeightOneSpectrum.adicCompletionComapAlgHom_map_closure_is_closed`, `IsDedekindDomain.HeightOneSpectrum.tensorAdicCompletionComapLinearMap_surjective`, `IsDedekindDomain.HeightOneSpectrum.adicCompletionTensorIntegerCoe_tmul`, `IsDedekindDomain.HeightOneSpectrum.tensorAdicCompletionComapAlgHom_tmul_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsScalarTowerWithVal_fLT` 📖	mathematical	—	`instAlgebraWithVal_fLT`	—	—
`instIsScalarTowerWithVal_fLT_1` 📖	—	—	—	—	—

---

← Back to Index