Commit 2025-08-25 04:06 6bc16791

View on Github →

feat(RingTheory/AdicValuation): valuation_surjective (#27109) for both the base valuation and the one on the extension

Estimated changes

Modified Mathlib/RingTheory/DedekindDomain/AdicValuation.lean

added theorem IsDedekindDomain.HeightOneSpectrum.valuation_surjective

added theorem IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_surjective

Modified Mathlib/Topology/Algebra/Valued/ValuedField.lean

added theorem Valued.valuedCompletion_surjective_iff