Blueprint Summary🔗

Overview

Total entries46completed: 45; deps incomplete: 0; sorries: 0; no proof: 1

Ready now0Entries whose next formalization step is currently unblocked.

Fully closed45Local code and prerequisite closure are both complete.

Actionable priorities0Entries ready now and already unlocking downstream work.

Entry index (46)

Definitions21completed: 21; deps incomplete: 0; sorries: 0; no proof: 0

Theorems25completed: 24; deps incomplete: 0; sorries: 0; no proof: 1

Informal-only entries1

Definition Index (21)

«huber-ring»(Definition)
Associated lean decls (2)
- PairOfDefinition
- IsHuberRing
«valuation-coarsening»(Definition)
Associated lean decls (1)
- Valuation.coarsen
«spv-comap»(Definition)
Associated lean decls (1)
- ValuationSpectrum.comap
«huber-pow-open»(Definition)
Associated lean decls (2)
- PairOfDefinition.pow_isOpen
- PairOfDefinition.isBounded_A₀
«characteristic-subgroup»(Definition)
Associated lean decls (2)
- Valuation.cGammaIdeal
- Valuation.imageGeOne
«affinoid-ring»(Definition)
Associated lean decls (2)
- ValuationSpectrum.IsRingOfIntegralElements
- ValuationSpectrum.IsAffinoidRing
«spv-ai»(Definition)
Associated lean decls (2)
- ValuationSpectrum.Spv.IsInSpvAI
- Valuation.CofinalValue
«rational-subsets»(Definition)
Associated lean decls (2)
- ValuationSpectrum.rationalOpen
- ValuationSpectrum.IsRationalSubset
«tate-algebra»(Definition)
Associated lean decls (2)
- TateAlgebra
- LaurentTateAlgebra
«convex-subgroup»(Definition)
Associated lean decls (2)
- ConvexSubgroup
- ConvexSubgroup.minContain
«continuous-valuation»(Definition)
Associated lean decls (2)
- Valuation.IsContinuous
- ValuationSpectrum.Cont
«spa-topcat»(Definition)
Associated lean decls (2)
- ValuationSpectrum.SpaTop
- ValuationSpectrum.suppSpa
«uniform-pair»(Definition)
Associated lean decls (2)
- TopologicalRing.IsUniform
- TopologicalRing.IsStablyUniform
«adic-spectrum»(Definition)
Associated lean decls (2)
- ValuationSpectrum.Spa
- ValuationSpectrum.PlusSubring
«analytic-points»(Definition)
Associated lean decls (3)
«restricted-power-series»(Definition)
Associated lean decls (3)
«pseudo-uniformizer»(Definition)
Associated lean decls (2)
- IsPseudoUniformizer
- PseudoUniformizer
«power-bounded»(Definition)
Associated lean decls (2)
- TopologicalRing.powerBoundedSubring
- TopologicalRing.topologicallyNilpotentElements
«valuation-spectrum»(Definition)
Associated lean decls (3)
«convex-valuation-link»(Definition)
Associated lean decls (1)
- Valuation.restrictToConvex
«tate-ring»(Definition)
Associated lean decls (1)
- IsTateRing

Theorem / Proposition / Lemma / Corollary Index (25)

«structure-presheaf-typelevel-sheaf»(Theorem)
Associated lean decls (1)
- ValuationSpectrum.structurePresheaf_typeLevel_isSheaf
«spa-compact»(Theorem)
Associated lean decls (2)
- ValuationSpectrum.isCompact_spa_of_tate_pseudouniformizer
- ValuationSpectrum.instCompactSpace_spa
«rational-subsets-open»(Theorem)
Associated lean decls (2)
- ValuationSpectrum.IsRationalSubset.isOpen
- ValuationSpectrum.rationalOpen_isOpen
«tate-open-nilradical»(Theorem)
Associated lean decls (1)
- IsTateRing.isOpen_topologicalNilradical
«maximal-open-implies-closed»(Theorem)
Associated lean decls (2)
- IsTopologicallyNilpotent.mem_of_isMaximal
- isOpen_of_isMaximal_of_isOpen_topologicallyNilpotent
«power-bounded-integrally-closed»(Theorem)
Associated lean decls (1)
- TopologicalRing.IsBounded.isPowerBounded_of_isIntegral
«continuity-via-restriction»(Theorem)
Associated lean decls (2)
- Valuation.restrictToConvex
- PairOfDefinition.isContinuous_of_restriction_isContinuous
«tate-algebra-eval»(Theorem)
Associated lean decls (2)
- TateAlgebra.evalZeroHom
- TateAlgebra.evalZeroHom_surjective
«laurent-zeta-unit»(Theorem)
Associated lean decls (2)
- LaurentTateAlgebra.zeta_mul_zetaInv
- LaurentTateAlgebra.zetaInv_mul_zeta
«cor-732-dominating-unit»(Theorem)
Associated lean decls (1)
- ValuationSpectrum.exists_dominating_unit
«supp-continuous»(Theorem)
Associated lean decls (2)
- ValuationSpectrum.suppFun
- ValuationSpectrum.suppFun_continuous
«analytic-adic-complete»(Theorem)
Associated lean decls (2)
- PairOfDefinition.I_le_maximal_of_isAdicComplete
- PairOfDefinition.not_isMaximal_of_I_not_le
«continuous-injectivity»(Theorem)
Associated lean decls (2)
- Valuation.isEquiv_of_isContinuous_of_denseRange
- ValuationSpectrum.eq_of_isContinuous_of_comap_eq_of_denseRange
«rational-subsets-inter»(Theorem)
Associated lean decls (2)
- ValuationSpectrum.IsRationalSubset.inter
- ValuationSpectrum.rationalOpen_inter
«closed-ideal-noetherian»(Theorem)
Associated lean decls (1)
- Wedhorn.isClosed_ideal_of_noetherian
«spv-compact»(Theorem)
Associated lean decls (2)
- ValuationSpectrum.ιSpv_isEmbedding
- ValuationSpectrum.compactSpace_of_subbasic_subcover
«open-ideal-criterion»(Theorem)
Associated lean decls (1)
- ideal_isOpen_iff_topologicalNilradical_le_radical
«spa-supp-maximal»(Theorem)
Associated lean decls (2)
- ValuationSpectrum.exists_mem_spa_supp_eq
- ValuationSpectrum.exists_mem_spa_supp_eq_of_isOpen_topologicallyNilpotent
«structure-sheaf»(Theorem)
«module-open-mapping»(Theorem)
Associated lean decls (2)
- IsModuleTopology.isOpenMap_of_surjective_of_finite
- IsModuleTopology.strictExact
«spa-functorial»(Theorem)
Associated lean decls (2)
- ValuationSpectrum.spaComap
- ValuationSpectrum.comap_mem_spa
«tate-all-analytic»(Theorem)
Associated lean decls (1)
- ValuationSpectrum.IsTateRing.isAnalytic
«lemma-745-nonopen-support»(Theorem)
Associated lean decls (1)
- PairOfDefinition.exists_mem_spa_supp_ge_of_nonOpen_prime
«integral-le-powerbounded»(Theorem)
Associated lean decls (2)
- ValuationSpectrum.IsRingOfIntegralElements.le_powerBoundedSubring
- ValuationSpectrum.IsRingOfIntegralElements.topologicallyNilpotentElements_subset
«power-bounded-add»(Theorem)
Associated lean decls (1)
- TopologicalRing.isPowerBounded_add

Dependency insights

Statement-used entries23Entries reused in statement dependencies.

Proof-used entries5Entries reused in proof-only dependencies.

Most used in statements (23)

«tate-ring»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 8proof uses: 0direct uses: 8downstream unlocks: 11
Associated lean decls (1)
- IsTateRing
«huber-ring»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 7proof uses: 0direct uses: 7downstream unlocks: 29
Associated lean decls (2)
- PairOfDefinition
- IsHuberRing
«adic-spectrum»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 7proof uses: 0direct uses: 7downstream unlocks: 17
Associated lean decls (2)
- ValuationSpectrum.Spa
- ValuationSpectrum.PlusSubring
«power-bounded»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 24
Associated lean decls (2)
- TopologicalRing.powerBoundedSubring
- TopologicalRing.topologicallyNilpotentElements
«rational-subsets»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 7
Associated lean decls (2)
- ValuationSpectrum.rationalOpen
- ValuationSpectrum.IsRationalSubset
«valuation-spectrum»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 25
Associated lean decls (3)
«continuous-valuation»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 21
Associated lean decls (2)
- Valuation.IsContinuous
- ValuationSpectrum.Cont
«affinoid-ring»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 20
Associated lean decls (2)
- ValuationSpectrum.IsRingOfIntegralElements
- ValuationSpectrum.IsAffinoidRing
«convex-subgroup»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 5
Associated lean decls (2)
- ConvexSubgroup
- ConvexSubgroup.minContain
«tate-algebra»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 3
Associated lean decls (2)
- TateAlgebra
- LaurentTateAlgebra
Show all 13 more statement-used entries
- «pseudo-uniformizer»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 1direct uses: 3downstream unlocks: 2
  Associated lean decls (2)
  - IsPseudoUniformizer
  - PseudoUniformizer
- «analytic-points»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
  Associated lean decls (3)
- «convex-valuation-link»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
  Associated lean decls (1)
  - Valuation.restrictToConvex
- «spv-comap»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
  Associated lean decls (1)
  - ValuationSpectrum.comap
- «restricted-power-series»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 4
  Associated lean decls (3)
- «supp-continuous»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (2)
  - ValuationSpectrum.suppFun
  - ValuationSpectrum.suppFun_continuous
- «spv-compact»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 2
  Associated lean decls (2)
  - ValuationSpectrum.ιSpv_isEmbedding
  - ValuationSpectrum.compactSpace_of_subbasic_subcover
- «spa-topcat»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (2)
  - ValuationSpectrum.SpaTop
  - ValuationSpectrum.suppSpa
- «module-open-mapping»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 1
  Associated lean decls (2)
  - IsModuleTopology.isOpenMap_of_surjective_of_finite
  - IsModuleTopology.strictExact
- «open-ideal-criterion»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 1
  Associated lean decls (1)
  - ideal_isOpen_iff_topologicalNilradical_le_radical
- «spa-compact»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 1
  Associated lean decls (2)
  - ValuationSpectrum.isCompact_spa_of_tate_pseudouniformizer
  - ValuationSpectrum.instCompactSpace_spa
- «structure-presheaf-typelevel-sheaf»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - ValuationSpectrum.structurePresheaf_typeLevel_isSheaf
- «uniform-pair»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (2)
  - TopologicalRing.IsUniform
  - TopologicalRing.IsStablyUniform

Most used in proofs (5)

«pseudo-uniformizer»(Definition)

Reverse dependencies recorded in proof dependencies.

proof uses: 1statement uses: 2direct uses: 3downstream unlocks: 2
Associated lean decls (2)
- IsPseudoUniformizer
- PseudoUniformizer
«spv-compact»(Theorem)

Reverse dependencies recorded in proof dependencies.

proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 2
Associated lean decls (2)
- ValuationSpectrum.ιSpv_isEmbedding
- ValuationSpectrum.compactSpace_of_subbasic_subcover
«module-open-mapping»(Theorem)

Reverse dependencies recorded in proof dependencies.

proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 1
Associated lean decls (2)
- IsModuleTopology.isOpenMap_of_surjective_of_finite
- IsModuleTopology.strictExact
«open-ideal-criterion»(Theorem)

Reverse dependencies recorded in proof dependencies.

proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 1
Associated lean decls (1)
- ideal_isOpen_iff_topologicalNilradical_le_radical
«spa-compact»(Theorem)

Reverse dependencies recorded in proof dependencies.

proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 1
Associated lean decls (2)
- ValuationSpectrum.isCompact_spa_of_tate_pseudouniformizer
- ValuationSpectrum.instCompactSpace_spa

Metadata

Metadata audit

Missing owner46

Missing effort46

Untagged46

Missing owner (46)

«adic-spectrum»(Definition)

Missing owner metadata.
Associated lean decls (2)
- ValuationSpectrum.Spa
- ValuationSpectrum.PlusSubring
«affinoid-ring»(Definition)

Missing owner metadata.
Associated lean decls (2)
- ValuationSpectrum.IsRingOfIntegralElements
- ValuationSpectrum.IsAffinoidRing
«analytic-adic-complete»(Theorem)

Missing owner metadata.
Associated lean decls (2)
- PairOfDefinition.I_le_maximal_of_isAdicComplete
- PairOfDefinition.not_isMaximal_of_I_not_le
«analytic-points»(Definition)

Missing owner metadata.
Associated lean decls (3)
«characteristic-subgroup»(Definition)

Missing owner metadata.
Associated lean decls (2)
- Valuation.cGammaIdeal
- Valuation.imageGeOne
«closed-ideal-noetherian»(Theorem)

Missing owner metadata.
Associated lean decls (1)
- Wedhorn.isClosed_ideal_of_noetherian
«continuity-via-restriction»(Theorem)

Missing owner metadata.
Associated lean decls (2)
- Valuation.restrictToConvex
- PairOfDefinition.isContinuous_of_restriction_isContinuous
«continuous-injectivity»(Theorem)

Missing owner metadata.
Associated lean decls (2)
- Valuation.isEquiv_of_isContinuous_of_denseRange
- ValuationSpectrum.eq_of_isContinuous_of_comap_eq_of_denseRange
«continuous-valuation»(Definition)

Missing owner metadata.
Associated lean decls (2)
- Valuation.IsContinuous
- ValuationSpectrum.Cont
«convex-subgroup»(Definition)

Missing owner metadata.
Associated lean decls (2)
- ConvexSubgroup
- ConvexSubgroup.minContain
Show all 36 more entries missing owner
- «convex-valuation-link»(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Valuation.restrictToConvex
- «cor-732-dominating-unit»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - ValuationSpectrum.exists_dominating_unit
- «huber-pow-open»(Definition)
  
  Missing owner metadata.
  Associated lean decls (2)
  - PairOfDefinition.pow_isOpen
  - PairOfDefinition.isBounded_A₀
- «huber-ring»(Definition)
  
  Missing owner metadata.
  Associated lean decls (2)
  - PairOfDefinition
  - IsHuberRing
- «integral-le-powerbounded»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - ValuationSpectrum.IsRingOfIntegralElements.le_powerBoundedSubring
  - ValuationSpectrum.IsRingOfIntegralElements.topologicallyNilpotentElements_subset
- «laurent-zeta-unit»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - LaurentTateAlgebra.zeta_mul_zetaInv
  - LaurentTateAlgebra.zetaInv_mul_zeta
- «lemma-745-nonopen-support»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - PairOfDefinition.exists_mem_spa_supp_ge_of_nonOpen_prime
- «maximal-open-implies-closed»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - IsTopologicallyNilpotent.mem_of_isMaximal
  - isOpen_of_isMaximal_of_isOpen_topologicallyNilpotent
- «module-open-mapping»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - IsModuleTopology.isOpenMap_of_surjective_of_finite
  - IsModuleTopology.strictExact
- «open-ideal-criterion»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - ideal_isOpen_iff_topologicalNilradical_le_radical
- «power-bounded-add»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - TopologicalRing.isPowerBounded_add
- «power-bounded-integrally-closed»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - TopologicalRing.IsBounded.isPowerBounded_of_isIntegral
- «power-bounded»(Definition)
  
  Missing owner metadata.
  Associated lean decls (2)
  - TopologicalRing.powerBoundedSubring
  - TopologicalRing.topologicallyNilpotentElements
- «pseudo-uniformizer»(Definition)
  
  Missing owner metadata.
  Associated lean decls (2)
  - IsPseudoUniformizer
  - PseudoUniformizer
- «rational-subsets-inter»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - ValuationSpectrum.IsRationalSubset.inter
  - ValuationSpectrum.rationalOpen_inter
- «rational-subsets-open»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - ValuationSpectrum.IsRationalSubset.isOpen
  - ValuationSpectrum.rationalOpen_isOpen
- «rational-subsets»(Definition)
  
  Missing owner metadata.
  Associated lean decls (2)
  - ValuationSpectrum.rationalOpen
  - ValuationSpectrum.IsRationalSubset
- «restricted-power-series»(Definition)
  
  Missing owner metadata.
  Associated lean decls (3)
- «spa-compact»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - ValuationSpectrum.isCompact_spa_of_tate_pseudouniformizer
  - ValuationSpectrum.instCompactSpace_spa
- «spa-functorial»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - ValuationSpectrum.spaComap
  - ValuationSpectrum.comap_mem_spa
- «spa-supp-maximal»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - ValuationSpectrum.exists_mem_spa_supp_eq
  - ValuationSpectrum.exists_mem_spa_supp_eq_of_isOpen_topologicallyNilpotent
- «spa-topcat»(Definition)
  
  Missing owner metadata.
  Associated lean decls (2)
  - ValuationSpectrum.SpaTop
  - ValuationSpectrum.suppSpa
- «spv-ai»(Definition)
  
  Missing owner metadata.
  Associated lean decls (2)
  - ValuationSpectrum.Spv.IsInSpvAI
  - Valuation.CofinalValue
- «spv-comap»(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - ValuationSpectrum.comap
- «spv-compact»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - ValuationSpectrum.ιSpv_isEmbedding
  - ValuationSpectrum.compactSpace_of_subbasic_subcover
- «structure-presheaf-typelevel-sheaf»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - ValuationSpectrum.structurePresheaf_typeLevel_isSheaf
- «structure-sheaf»(Theorem)
  
  Missing owner metadata.
- «supp-continuous»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - ValuationSpectrum.suppFun
  - ValuationSpectrum.suppFun_continuous
- «tate-algebra-eval»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - TateAlgebra.evalZeroHom
  - TateAlgebra.evalZeroHom_surjective
- «tate-algebra»(Definition)
  
  Missing owner metadata.
  Associated lean decls (2)
  - TateAlgebra
  - LaurentTateAlgebra
- «tate-all-analytic»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - ValuationSpectrum.IsTateRing.isAnalytic
- «tate-open-nilradical»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - IsTateRing.isOpen_topologicalNilradical
- «tate-ring»(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - IsTateRing
- «uniform-pair»(Definition)
  
  Missing owner metadata.
  Associated lean decls (2)
  - TopologicalRing.IsUniform
  - TopologicalRing.IsStablyUniform
- «valuation-coarsening»(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Valuation.coarsen
- «valuation-spectrum»(Definition)
  
  Missing owner metadata.
  Associated lean decls (3)

Missing effort (46)

«adic-spectrum»(Definition)

Missing effort metadata.
Associated lean decls (2)
- ValuationSpectrum.Spa
- ValuationSpectrum.PlusSubring
«affinoid-ring»(Definition)

Missing effort metadata.
Associated lean decls (2)
- ValuationSpectrum.IsRingOfIntegralElements
- ValuationSpectrum.IsAffinoidRing
«analytic-adic-complete»(Theorem)

Missing effort metadata.
Associated lean decls (2)
- PairOfDefinition.I_le_maximal_of_isAdicComplete
- PairOfDefinition.not_isMaximal_of_I_not_le
«analytic-points»(Definition)

Missing effort metadata.
Associated lean decls (3)
«characteristic-subgroup»(Definition)

Missing effort metadata.
Associated lean decls (2)
- Valuation.cGammaIdeal
- Valuation.imageGeOne
«closed-ideal-noetherian»(Theorem)

Missing effort metadata.
Associated lean decls (1)
- Wedhorn.isClosed_ideal_of_noetherian
«continuity-via-restriction»(Theorem)

Missing effort metadata.
Associated lean decls (2)
- Valuation.restrictToConvex
- PairOfDefinition.isContinuous_of_restriction_isContinuous
«continuous-injectivity»(Theorem)

Missing effort metadata.
Associated lean decls (2)
- Valuation.isEquiv_of_isContinuous_of_denseRange
- ValuationSpectrum.eq_of_isContinuous_of_comap_eq_of_denseRange
«continuous-valuation»(Definition)

Missing effort metadata.
Associated lean decls (2)
- Valuation.IsContinuous
- ValuationSpectrum.Cont
«convex-subgroup»(Definition)

Missing effort metadata.
Associated lean decls (2)
- ConvexSubgroup
- ConvexSubgroup.minContain
Show all 36 more entries missing effort
- «convex-valuation-link»(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Valuation.restrictToConvex
- «cor-732-dominating-unit»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - ValuationSpectrum.exists_dominating_unit
- «huber-pow-open»(Definition)
  
  Missing effort metadata.
  Associated lean decls (2)
  - PairOfDefinition.pow_isOpen
  - PairOfDefinition.isBounded_A₀
- «huber-ring»(Definition)
  
  Missing effort metadata.
  Associated lean decls (2)
  - PairOfDefinition
  - IsHuberRing
- «integral-le-powerbounded»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - ValuationSpectrum.IsRingOfIntegralElements.le_powerBoundedSubring
  - ValuationSpectrum.IsRingOfIntegralElements.topologicallyNilpotentElements_subset
- «laurent-zeta-unit»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - LaurentTateAlgebra.zeta_mul_zetaInv
  - LaurentTateAlgebra.zetaInv_mul_zeta
- «lemma-745-nonopen-support»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - PairOfDefinition.exists_mem_spa_supp_ge_of_nonOpen_prime
- «maximal-open-implies-closed»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - IsTopologicallyNilpotent.mem_of_isMaximal
  - isOpen_of_isMaximal_of_isOpen_topologicallyNilpotent
- «module-open-mapping»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - IsModuleTopology.isOpenMap_of_surjective_of_finite
  - IsModuleTopology.strictExact
- «open-ideal-criterion»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - ideal_isOpen_iff_topologicalNilradical_le_radical
- «power-bounded-add»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - TopologicalRing.isPowerBounded_add
- «power-bounded-integrally-closed»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - TopologicalRing.IsBounded.isPowerBounded_of_isIntegral
- «power-bounded»(Definition)
  
  Missing effort metadata.
  Associated lean decls (2)
  - TopologicalRing.powerBoundedSubring
  - TopologicalRing.topologicallyNilpotentElements
- «pseudo-uniformizer»(Definition)
  
  Missing effort metadata.
  Associated lean decls (2)
  - IsPseudoUniformizer
  - PseudoUniformizer
- «rational-subsets-inter»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - ValuationSpectrum.IsRationalSubset.inter
  - ValuationSpectrum.rationalOpen_inter
- «rational-subsets-open»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - ValuationSpectrum.IsRationalSubset.isOpen
  - ValuationSpectrum.rationalOpen_isOpen
- «rational-subsets»(Definition)
  
  Missing effort metadata.
  Associated lean decls (2)
  - ValuationSpectrum.rationalOpen
  - ValuationSpectrum.IsRationalSubset
- «restricted-power-series»(Definition)
  
  Missing effort metadata.
  Associated lean decls (3)
- «spa-compact»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - ValuationSpectrum.isCompact_spa_of_tate_pseudouniformizer
  - ValuationSpectrum.instCompactSpace_spa
- «spa-functorial»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - ValuationSpectrum.spaComap
  - ValuationSpectrum.comap_mem_spa
- «spa-supp-maximal»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - ValuationSpectrum.exists_mem_spa_supp_eq
  - ValuationSpectrum.exists_mem_spa_supp_eq_of_isOpen_topologicallyNilpotent
- «spa-topcat»(Definition)
  
  Missing effort metadata.
  Associated lean decls (2)
  - ValuationSpectrum.SpaTop
  - ValuationSpectrum.suppSpa
- «spv-ai»(Definition)
  
  Missing effort metadata.
  Associated lean decls (2)
  - ValuationSpectrum.Spv.IsInSpvAI
  - Valuation.CofinalValue
- «spv-comap»(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - ValuationSpectrum.comap
- «spv-compact»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - ValuationSpectrum.ιSpv_isEmbedding
  - ValuationSpectrum.compactSpace_of_subbasic_subcover
- «structure-presheaf-typelevel-sheaf»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - ValuationSpectrum.structurePresheaf_typeLevel_isSheaf
- «structure-sheaf»(Theorem)
  
  Missing effort metadata.
- «supp-continuous»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - ValuationSpectrum.suppFun
  - ValuationSpectrum.suppFun_continuous
- «tate-algebra-eval»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - TateAlgebra.evalZeroHom
  - TateAlgebra.evalZeroHom_surjective
- «tate-algebra»(Definition)
  
  Missing effort metadata.
  Associated lean decls (2)
  - TateAlgebra
  - LaurentTateAlgebra
- «tate-all-analytic»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - ValuationSpectrum.IsTateRing.isAnalytic
- «tate-open-nilradical»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - IsTateRing.isOpen_topologicalNilradical
- «tate-ring»(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - IsTateRing
- «uniform-pair»(Definition)
  
  Missing effort metadata.
  Associated lean decls (2)
  - TopologicalRing.IsUniform
  - TopologicalRing.IsStablyUniform
- «valuation-coarsening»(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Valuation.coarsen
- «valuation-spectrum»(Definition)
  
  Missing effort metadata.
  Associated lean decls (3)

Untagged (46)

«adic-spectrum»(Definition)

Missing tag metadata.
Associated lean decls (2)
- ValuationSpectrum.Spa
- ValuationSpectrum.PlusSubring
«affinoid-ring»(Definition)

Missing tag metadata.
Associated lean decls (2)
- ValuationSpectrum.IsRingOfIntegralElements
- ValuationSpectrum.IsAffinoidRing
«analytic-adic-complete»(Theorem)

Missing tag metadata.
Associated lean decls (2)
- PairOfDefinition.I_le_maximal_of_isAdicComplete
- PairOfDefinition.not_isMaximal_of_I_not_le
«analytic-points»(Definition)

Missing tag metadata.
Associated lean decls (3)
«characteristic-subgroup»(Definition)

Missing tag metadata.
Associated lean decls (2)
- Valuation.cGammaIdeal
- Valuation.imageGeOne
«closed-ideal-noetherian»(Theorem)

Missing tag metadata.
Associated lean decls (1)
- Wedhorn.isClosed_ideal_of_noetherian
«continuity-via-restriction»(Theorem)

Missing tag metadata.
Associated lean decls (2)
- Valuation.restrictToConvex
- PairOfDefinition.isContinuous_of_restriction_isContinuous
«continuous-injectivity»(Theorem)

Missing tag metadata.
Associated lean decls (2)
- Valuation.isEquiv_of_isContinuous_of_denseRange
- ValuationSpectrum.eq_of_isContinuous_of_comap_eq_of_denseRange
«continuous-valuation»(Definition)

Missing tag metadata.
Associated lean decls (2)
- Valuation.IsContinuous
- ValuationSpectrum.Cont
«convex-subgroup»(Definition)

Missing tag metadata.
Associated lean decls (2)
- ConvexSubgroup
- ConvexSubgroup.minContain
Show all 36 more untagged entries
- «convex-valuation-link»(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Valuation.restrictToConvex
- «cor-732-dominating-unit»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - ValuationSpectrum.exists_dominating_unit
- «huber-pow-open»(Definition)
  
  Missing tag metadata.
  Associated lean decls (2)
  - PairOfDefinition.pow_isOpen
  - PairOfDefinition.isBounded_A₀
- «huber-ring»(Definition)
  
  Missing tag metadata.
  Associated lean decls (2)
  - PairOfDefinition
  - IsHuberRing
- «integral-le-powerbounded»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - ValuationSpectrum.IsRingOfIntegralElements.le_powerBoundedSubring
  - ValuationSpectrum.IsRingOfIntegralElements.topologicallyNilpotentElements_subset
- «laurent-zeta-unit»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - LaurentTateAlgebra.zeta_mul_zetaInv
  - LaurentTateAlgebra.zetaInv_mul_zeta
- «lemma-745-nonopen-support»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - PairOfDefinition.exists_mem_spa_supp_ge_of_nonOpen_prime
- «maximal-open-implies-closed»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - IsTopologicallyNilpotent.mem_of_isMaximal
  - isOpen_of_isMaximal_of_isOpen_topologicallyNilpotent
- «module-open-mapping»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - IsModuleTopology.isOpenMap_of_surjective_of_finite
  - IsModuleTopology.strictExact
- «open-ideal-criterion»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - ideal_isOpen_iff_topologicalNilradical_le_radical
- «power-bounded-add»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - TopologicalRing.isPowerBounded_add
- «power-bounded-integrally-closed»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - TopologicalRing.IsBounded.isPowerBounded_of_isIntegral
- «power-bounded»(Definition)
  
  Missing tag metadata.
  Associated lean decls (2)
  - TopologicalRing.powerBoundedSubring
  - TopologicalRing.topologicallyNilpotentElements
- «pseudo-uniformizer»(Definition)
  
  Missing tag metadata.
  Associated lean decls (2)
  - IsPseudoUniformizer
  - PseudoUniformizer
- «rational-subsets-inter»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - ValuationSpectrum.IsRationalSubset.inter
  - ValuationSpectrum.rationalOpen_inter
- «rational-subsets-open»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - ValuationSpectrum.IsRationalSubset.isOpen
  - ValuationSpectrum.rationalOpen_isOpen
- «rational-subsets»(Definition)
  
  Missing tag metadata.
  Associated lean decls (2)
  - ValuationSpectrum.rationalOpen
  - ValuationSpectrum.IsRationalSubset
- «restricted-power-series»(Definition)
  
  Missing tag metadata.
  Associated lean decls (3)
- «spa-compact»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - ValuationSpectrum.isCompact_spa_of_tate_pseudouniformizer
  - ValuationSpectrum.instCompactSpace_spa
- «spa-functorial»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - ValuationSpectrum.spaComap
  - ValuationSpectrum.comap_mem_spa
- «spa-supp-maximal»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - ValuationSpectrum.exists_mem_spa_supp_eq
  - ValuationSpectrum.exists_mem_spa_supp_eq_of_isOpen_topologicallyNilpotent
- «spa-topcat»(Definition)
  
  Missing tag metadata.
  Associated lean decls (2)
  - ValuationSpectrum.SpaTop
  - ValuationSpectrum.suppSpa
- «spv-ai»(Definition)
  
  Missing tag metadata.
  Associated lean decls (2)
  - ValuationSpectrum.Spv.IsInSpvAI
  - Valuation.CofinalValue
- «spv-comap»(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - ValuationSpectrum.comap
- «spv-compact»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - ValuationSpectrum.ιSpv_isEmbedding
  - ValuationSpectrum.compactSpace_of_subbasic_subcover
- «structure-presheaf-typelevel-sheaf»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - ValuationSpectrum.structurePresheaf_typeLevel_isSheaf
- «structure-sheaf»(Theorem)
  
  Missing tag metadata.
- «supp-continuous»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - ValuationSpectrum.suppFun
  - ValuationSpectrum.suppFun_continuous
- «tate-algebra-eval»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - TateAlgebra.evalZeroHom
  - TateAlgebra.evalZeroHom_surjective
- «tate-algebra»(Definition)
  
  Missing tag metadata.
  Associated lean decls (2)
  - TateAlgebra
  - LaurentTateAlgebra
- «tate-all-analytic»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - ValuationSpectrum.IsTateRing.isAnalytic
- «tate-open-nilradical»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - IsTateRing.isOpen_topologicalNilradical
- «tate-ring»(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - IsTateRing
- «uniform-pair»(Definition)
  
  Missing tag metadata.
  Associated lean decls (2)
  - TopologicalRing.IsUniform
  - TopologicalRing.IsStablyUniform
- «valuation-coarsening»(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Valuation.coarsen
- «valuation-spectrum»(Definition)
  
  Missing tag metadata.
  Associated lean decls (3)

Structure and coverage

Informal-only1Statements with no associated Lean code yet.

Fully closed45Local code and ancestor closure are both complete.

Heaviest prerequisites (41)

«structure-sheaf»(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
«spa-compact»(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 3statement deps: 3proof deps: 1direct uses: 2downstream unlocks: 1
Associated lean decls (2)
- ValuationSpectrum.isCompact_spa_of_tate_pseudouniformizer
- ValuationSpectrum.instCompactSpace_spa
«tate-all-analytic»(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 3statement deps: 3proof deps: 1direct uses: 0downstream unlocks: 0
Associated lean decls (1)
- ValuationSpectrum.IsTateRing.isAnalytic
«continuity-via-restriction»(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (2)
- Valuation.restrictToConvex
- PairOfDefinition.isContinuous_of_restriction_isContinuous
«lemma-745-nonopen-support»(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (1)
- PairOfDefinition.exists_mem_spa_supp_ge_of_nonOpen_prime
«tate-algebra»(Definition)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 3statement deps: 3proof deps: 0direct uses: 3downstream unlocks: 3
Associated lean decls (2)
- TateAlgebra
- LaurentTateAlgebra
«closed-ideal-noetherian»(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 2statement deps: 2proof deps: 1direct uses: 0downstream unlocks: 0
Associated lean decls (1)
- Wedhorn.isClosed_ideal_of_noetherian
«cor-732-dominating-unit»(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 2statement deps: 2proof deps: 1direct uses: 0downstream unlocks: 0
Associated lean decls (1)
- ValuationSpectrum.exists_dominating_unit
«maximal-open-implies-closed»(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 2statement deps: 2proof deps: 1direct uses: 0downstream unlocks: 0
Associated lean decls (2)
- IsTopologicallyNilpotent.mem_of_isMaximal
- isOpen_of_isMaximal_of_isOpen_topologicallyNilpotent
«adic-spectrum»(Definition)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 2statement deps: 2proof deps: 0direct uses: 7downstream unlocks: 17
Associated lean decls (2)
- ValuationSpectrum.Spa
- ValuationSpectrum.PlusSubring
Show all 31 more heaviest-prerequisite entries
- «affinoid-ring»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 3downstream unlocks: 20
  Associated lean decls (2)
  - ValuationSpectrum.IsRingOfIntegralElements
  - ValuationSpectrum.IsAffinoidRing
- «analytic-adic-complete»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (2)
  - PairOfDefinition.I_le_maximal_of_isAdicComplete
  - PairOfDefinition.not_isMaximal_of_I_not_le
- «continuous-injectivity»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (2)
  - Valuation.isEquiv_of_isContinuous_of_denseRange
  - ValuationSpectrum.eq_of_isContinuous_of_comap_eq_of_denseRange
- «integral-le-powerbounded»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (2)
  - ValuationSpectrum.IsRingOfIntegralElements.le_powerBoundedSubring
  - ValuationSpectrum.IsRingOfIntegralElements.topologicallyNilpotentElements_subset
- «spa-functorial»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (2)
  - ValuationSpectrum.spaComap
  - ValuationSpectrum.comap_mem_spa
- «spa-topcat»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (2)
  - ValuationSpectrum.SpaTop
  - ValuationSpectrum.suppSpa
- «structure-presheaf-typelevel-sheaf»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - ValuationSpectrum.structurePresheaf_typeLevel_isSheaf
- «tate-open-nilradical»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - IsTateRing.isOpen_topologicalNilradical
- «uniform-pair»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (2)
  - TopologicalRing.IsUniform
  - TopologicalRing.IsStablyUniform
- «analytic-points»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 2
  Associated lean decls (3)
- «characteristic-subgroup»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (2)
  - Valuation.cGammaIdeal
  - Valuation.imageGeOne
- «continuous-valuation»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 4downstream unlocks: 21
  Associated lean decls (2)
  - Valuation.IsContinuous
  - ValuationSpectrum.Cont
- «convex-valuation-link»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 2
  Associated lean decls (1)
  - Valuation.restrictToConvex
- «huber-pow-open»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (2)
  - PairOfDefinition.pow_isOpen
  - PairOfDefinition.isBounded_A₀
- «laurent-zeta-unit»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (2)
  - LaurentTateAlgebra.zeta_mul_zetaInv
  - LaurentTateAlgebra.zetaInv_mul_zeta
- «module-open-mapping»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 1
  Associated lean decls (2)
  - IsModuleTopology.isOpenMap_of_surjective_of_finite
  - IsModuleTopology.strictExact
- «power-bounded-add»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - TopologicalRing.isPowerBounded_add
- «power-bounded-integrally-closed»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - TopologicalRing.IsBounded.isPowerBounded_of_isIntegral
- «pseudo-uniformizer»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 2
  Associated lean decls (2)
  - IsPseudoUniformizer
  - PseudoUniformizer
- «rational-subsets-inter»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (2)
  - ValuationSpectrum.IsRationalSubset.inter
  - ValuationSpectrum.rationalOpen_inter
- «rational-subsets-open»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (2)
  - ValuationSpectrum.IsRationalSubset.isOpen
  - ValuationSpectrum.rationalOpen_isOpen
- «rational-subsets»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 5downstream unlocks: 7
  Associated lean decls (2)
  - ValuationSpectrum.rationalOpen
  - ValuationSpectrum.IsRationalSubset
- «restricted-power-series»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 4
  Associated lean decls (3)
- «spa-supp-maximal»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (2)
  - ValuationSpectrum.exists_mem_spa_supp_eq
  - ValuationSpectrum.exists_mem_spa_supp_eq_of_isOpen_topologicallyNilpotent
- «spv-ai»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (2)
  - ValuationSpectrum.Spv.IsInSpvAI
  - Valuation.CofinalValue
- «spv-comap»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 2
  Associated lean decls (1)
  - ValuationSpectrum.comap
- «spv-compact»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 2
  Associated lean decls (2)
  - ValuationSpectrum.ιSpv_isEmbedding
  - ValuationSpectrum.compactSpace_of_subbasic_subcover
- «supp-continuous»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (2)
  - ValuationSpectrum.suppFun
  - ValuationSpectrum.suppFun_continuous
- «tate-algebra-eval»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (2)
  - TateAlgebra.evalZeroHom
  - TateAlgebra.evalZeroHom_surjective
- «tate-ring»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 8downstream unlocks: 11
  Associated lean decls (1)
  - IsTateRing
- «valuation-coarsening»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - Valuation.coarsen

No prerequisites (5)

«convex-subgroup»(Definition)
Associated lean decls (2)
- ConvexSubgroup
- ConvexSubgroup.minContain
«open-ideal-criterion»(Theorem)
Associated lean decls (1)
- ideal_isOpen_iff_topologicalNilradical_le_radical
«valuation-spectrum»(Definition)
Associated lean decls (3)
«power-bounded»(Definition)
Associated lean decls (2)
- TopologicalRing.powerBoundedSubring
- TopologicalRing.topologicallyNilpotentElements
«huber-ring»(Definition)
Associated lean decls (2)
- PairOfDefinition
- IsHuberRing

No dependents (23)

«spv-ai»(Definition)
Associated lean decls (2)
- ValuationSpectrum.Spv.IsInSpvAI
- Valuation.CofinalValue
«continuous-injectivity»(Theorem)
Associated lean decls (2)
- Valuation.isEquiv_of_isContinuous_of_denseRange
- ValuationSpectrum.eq_of_isContinuous_of_comap_eq_of_denseRange
«rational-subsets-inter»(Theorem)
Associated lean decls (2)
- ValuationSpectrum.IsRationalSubset.inter
- ValuationSpectrum.rationalOpen_inter
«closed-ideal-noetherian»(Theorem)
Associated lean decls (1)
- Wedhorn.isClosed_ideal_of_noetherian
«structure-sheaf»(Theorem)
«spa-functorial»(Theorem)
Associated lean decls (2)
- ValuationSpectrum.spaComap
- ValuationSpectrum.comap_mem_spa
«tate-all-analytic»(Theorem)
Associated lean decls (1)
- ValuationSpectrum.IsTateRing.isAnalytic
«lemma-745-nonopen-support»(Theorem)
Associated lean decls (1)
- PairOfDefinition.exists_mem_spa_supp_ge_of_nonOpen_prime
«integral-le-powerbounded»(Theorem)
Associated lean decls (2)
- ValuationSpectrum.IsRingOfIntegralElements.le_powerBoundedSubring
- ValuationSpectrum.IsRingOfIntegralElements.topologicallyNilpotentElements_subset
«power-bounded-add»(Theorem)
Associated lean decls (1)
- TopologicalRing.isPowerBounded_add
Show all 13 more entries without dependents
- «spa-supp-maximal»(Theorem)
  Associated lean decls (2)
  - ValuationSpectrum.exists_mem_spa_supp_eq
  - ValuationSpectrum.exists_mem_spa_supp_eq_of_isOpen_topologicallyNilpotent
- «characteristic-subgroup»(Definition)
  Associated lean decls (2)
  - Valuation.cGammaIdeal
  - Valuation.imageGeOne
- «analytic-adic-complete»(Theorem)
  Associated lean decls (2)
  - PairOfDefinition.I_le_maximal_of_isAdicComplete
  - PairOfDefinition.not_isMaximal_of_I_not_le
- «huber-pow-open»(Definition)
  Associated lean decls (2)
  - PairOfDefinition.pow_isOpen
  - PairOfDefinition.isBounded_A₀
- «cor-732-dominating-unit»(Theorem)
  Associated lean decls (1)
  - ValuationSpectrum.exists_dominating_unit
- «laurent-zeta-unit»(Theorem)
  Associated lean decls (2)
  - LaurentTateAlgebra.zeta_mul_zetaInv
  - LaurentTateAlgebra.zetaInv_mul_zeta
- «valuation-coarsening»(Definition)
  Associated lean decls (1)
  - Valuation.coarsen
- «tate-algebra-eval»(Theorem)
  Associated lean decls (2)
  - TateAlgebra.evalZeroHom
  - TateAlgebra.evalZeroHom_surjective
- «continuity-via-restriction»(Theorem)
  Associated lean decls (2)
  - Valuation.restrictToConvex
  - PairOfDefinition.isContinuous_of_restriction_isContinuous
- «power-bounded-integrally-closed»(Theorem)
  Associated lean decls (1)
  - TopologicalRing.IsBounded.isPowerBounded_of_isIntegral
- «maximal-open-implies-closed»(Theorem)
  Associated lean decls (2)
  - IsTopologicallyNilpotent.mem_of_isMaximal
  - isOpen_of_isMaximal_of_isOpen_topologicallyNilpotent
- «tate-open-nilradical»(Theorem)
  Associated lean decls (1)
  - IsTateRing.isOpen_topologicalNilradical
- «rational-subsets-open»(Theorem)
  Associated lean decls (2)
  - ValuationSpectrum.IsRationalSubset.isOpen
  - ValuationSpectrum.rationalOpen_isOpen