Theorem Units.mulArchimedean_iff

Modification history

2025-07-31 22:37
Mathlib/GroupTheory/ArchimedeanDensely.lean
feat(Valued/LocallyCompact): do not require RankOne to show IsDVR (#27412) …
Added Units.mulArchimedean_iffView on Github →