Theorem Valuation.closure_image_coe_ofPred_map_mul_map_lt_map

Modification history

2026-09-25 16:01
Mathlib/Topology/Algebra/ValuativeRel/Completion.lean
feat(Valued/ValuationTopology): creating instances of `IsValuativeTopology` on completion (#36769) …
Added Valuation.closure_image_coe_ofPred_map_mul_map_lt_mapView on Github →