Commit 2025-08-07 17:04 cd9f3f69

View on Github →

feat(Valued): FaithfulSMul to completion (#27116) simplifies coercions and golfs existing instance

Estimated changes

Modified Mathlib/RingTheory/DedekindDomain/AdicValuation.lean

added theorem IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletionIntegers_apply

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