Theorem Valued.closure_coe_completion_v_mul_v_lt

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.closure_coe_completion_v_mul_v_ltView on Github →