Theorem Valued.coe_valuation_eq_rankOne_hom_comp_valuation

Modification history

2026-03-06 13:45
Mathlib/Topology/Algebra/Valued/NormedValued.lean
chore(RingTheory/Valuation/RankOne): modify the definition of Valuation.RankOne using its range rather than its codomain (#26872) …
Modified Valued.coe_valuation_eq_rankOne_hom_comp_valuationView on Github →
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 →