Theorem Valued.integer.mulArchimedean_mrange_of_isCompact_integer

Modification history

2025-07-31 22:37
Mathlib/Topology/Algebra/Valued/LocallyCompact.lean
feat(Valued/LocallyCompact): do not require RankOne to show IsDVR (#27412) …
Added Valued.integer.mulArchimedean_mrange_of_isCompact_integerView on Github →