Theorem Valued.valuedCompletion_surjective_iff

Modification history

2025-08-25 04:06
Mathlib/Topology/Algebra/Valued/ValuedField.lean
feat(RingTheory/AdicValuation): valuation_surjective (#27109) …
Added Valued.valuedCompletion_surjective_iffView on Github →