Theorem Valued.exists_coe_eq_v

Modification history

2025-08-10 15:01
Mathlib/Topology/Algebra/Valued/ValuedField.lean
feat(Topology/ValuedField): range of valuation on competion is the same as base field (#27264) …
Added Valued.exists_coe_eq_vView on Github →