Theorem ValuativeRel.IsRankLeOne.of_compatible_mulArchimedean

Modification history

2025-07-31 23:29
Mathlib/RingTheory/Valuation/RankOne.lean
feat(RingTheory/ValuativeRel): IsRankLeOne when there is a compatible Zm0 or NNReal valuation (#27183) …
Added ValuativeRel.IsRankLeOne.of_compatible_mulArchimedeanView on Github →