Theorem Valued.extensionValuation_apply_coe

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