Theorem Valuation.exists_div_eq_of_surjective

Modification history

2026-06-03 06:54
Mathlib/Topology/Algebra/Valued/WithVal.lean
feat(Valuation/ValuativeRel): generalize `ValuativeRel` to non-commutative rings (#36777) …
Modified Valuation.exists_div_eq_of_surjectiveView on Github →
2025-12-19 16:47
Mathlib/Topology/Algebra/Valued/WithVal.lean
feat: `adicCompletion` for `Rat` is uniform isomorphic to `Padic` (#30576)
Added Valuation.exists_div_eq_of_surjectiveView on Github →