Theorem Valued.coe_valuation_eq_rankOne_hom_comp_valuation

Modification history

2024-10-22 04:01
Mathlib/Topology/Algebra/Valued/NormedValued.lean
chore(Topology/Algebra/Valued/NormedValued): rely on TC IsUltrametricDist instead of explicit arg (#17561) …
Added Valued.coe_valuation_eq_rankOne_hom_comp_valuationView on Github →