feat(RingTheory/Valuation): define the valuation spectrum and its topology#38009

Open

CBirkbeck wants to merge 15 commits intoleanprover-community:masterfrom

CBirkbeck:feat/valuation-spectrum

Commits on Apr 13, 2026

feat(RingTheory/Valuation): define the valuation spectrum and its topology

CBirkbeck
and
claude
committed
doc(ValuationSpectrum): explain the design choice to extend ValuativeRel

CBirkbeck
and
claude
committed
chore(ValuationSpectrum): remove redundant Wedhorn references from docstrings

CBirkbeck
and
claude
committed
style(ValuationSpectrum): move design note from docstring to comment

CBirkbeck
and
claude
committed
style(ValuationSpectrum): remove inline Wedhorn references from docstrings

CBirkbeck
and
claude
committed
some golfs
CBirkbeck
committed
style(ValuationSpectrum): remove subsection headers

CBirkbeck
and
claude
committed
style(ValuativeRel/Comap): fix line length in docstring

CBirkbeck
and
claude
committed
style(ValuationSpectrum): use ↦ instead of => for consistency

CBirkbeck
and
claude
committed
fix(ValuationSpectrum): add module declarations for Lean 4 module system

CBirkbeck
and
claude
committed

Commits on Apr 14, 2026